1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
5 -/
6 import topology.maps
src └───────────┘
7
8 /-!
9 # Constructions of new topological spaces from old ones
10
11 This file constructs products, sums, subtypes and quotients of topological spaces
12 and sets up their basic theory, such as criteria for maps into or out of these
13 constructions to be continuous; descriptions of the open sets, neighborhood filters,
14 and generators of these constructions; and their behavior with respect to embeddings
15 and other specific classes of maps.
16
17 ## Implementation note
18
19 The constructed topologies are defined using induced and coinduced topologies
20 along with the complete lattice structure on topologies. Their universal properties
21 (for example, a map `X → Y × Z` is continuous if and only if both projections
22 `X → Y`, `X → Z` are) follow easily using order-theoretic descriptions of
23 continuity. With more work we can also extract descriptions of the open sets,
24 neighborhood filters and so on.
25
26 ## Tags
27
28 product, sum, disjoint union, subspace, quotient space
29
30 -/
31
32 noncomputable theory
33
34 open topological_space set filter lattice
35 open_locale classical topological_space
36
37 universes u v w x
38 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
39
40 section constructions
41
42 instance {p : α → Prop} [t : topological_space α] : topological_space (subtype p) :=
id ┴ └───────────────┘ ┴ └───────────────┘ └─────┘ ┴
src └───────────────┘ └───────────────┘ └─────┘
typ ┴ └───────────────┘ ┴ └───────────────┘ └─────┘ ┴
doc └───────────────┘ └───────────────┘
43 induced subtype.val t
id └─────┘ └─────────┘ ┴
src └─────┘ └─────────┘
typ └─────┘ └─────────┘ ┴
doc └─────┘
44
45 instance {r : α → α → Prop} [t : topological_space α] : topological_space (quot r) :=
id ┴ ┴ └───────────────┘ ┴ └───────────────┘ └──┘ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ └───────────────┘ └──┘ ┴
doc └───────────────┘ └───────────────┘
46 coinduced (quot.mk r) t
id └───────┘ └─────┘ ┴ ┴
src └───────┘
typ └───────┘ └─────┘ ┴ ┴
doc └───────┘
47
48 instance {s : setoid α} [t : topological_space α] : topological_space (quotient s) :=
id └────┘ ┴ └───────────────┘ ┴ └───────────────┘ └──────┘ ┴
src └────┘ └───────────────┘ └───────────────┘ └──────┘
typ └────┘ ┴ └───────────────┘ ┴ └───────────────┘ └──────┘ ┴
doc └───────────────┘ └───────────────┘
49 coinduced quotient.mk t
id └───────┘ └─────────┘ ┴
src └───────┘ └─────────┘
typ └───────┘ └─────────┘ ┴
doc └───────┘
50
51 instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α × β) :=
id └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘ └───────────────┘ └───────────────┘ ┴
typ └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘ └───────────────┘ └───────────────┘
52 induced prod.fst t₁ ⊓ induced prod.snd t₂
id └─────┘ └──────┘ └┘ ┴ └─────┘ └──────┘ └┘
src └─────┘ └──────┘ ┴ └─────┘ └──────┘
typ └─────┘ └──────┘ └┘ ┴ └─────┘ └──────┘ └┘
doc └─────┘ └─────┘
53
54 instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α ⊕ β) :=
id └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘ └───────────────┘ └───────────────┘ ┴
typ └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘ └───────────────┘ └───────────────┘
55 coinduced sum.inl t₁ ⊔ coinduced sum.inr t₂
id └───────┘ └─────┘ └┘ ┴ └───────┘ └─────┘ └┘
src └───────┘ └─────┘ ┴ └───────┘ └─────┘
typ └───────┘ └─────┘ └┘ ┴ └───────┘ └─────┘ └┘
doc └───────┘ └───────┘
56
57 instance {β : α → Type v} [t₂ : Πa, topological_space (β a)] : topological_space (sigma β) :=
id ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ └───┘ ┴
src └───────────────┘ └───────────────┘ └───┘
typ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ └───┘ ┴
doc └───────────────┘ └───────────────┘
58 ⨆a, coinduced (sigma.mk a) (t₂ a)
id ┴┴┴ └───────┘ └──────┘ ┴ └┘ ┴
src ┴ ┴ └───────┘ └──────┘
typ ┴┴┴ └───────┘ └──────┘ ┴ └┘ ┴
doc ┴ ┴ └───────┘
59
60 instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_space (β a)] :
id ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘
61 topological_space (Πa, β a) :=
id └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘
62 ⨅a, induced (λf, f a) (t₂ a)
id ┴┴┴ └─────┘ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └─────┘
typ ┴┴┴ └─────┘ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴ └─────┘
63
64 lemma quotient_dense_of_dense [setoid α] [topological_space α] {s : set α} (H : ∀ x, x ∈ closure s) :
id └────┘ ┴ └───────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └────┘ └───────────────┘ └─┘ ┴ └─────┘
typ └────┘ ┴ └───────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └───────────────┘ └─────┘
65 closure (quotient.mk '' s) = univ :=
id └─────┘ └─────────┘ └┘ ┴ ┴ └──┘
src └─────┘ └─────────┘ └┘ ┴ └──┘
typ └─────┘ └─────────┘ └┘ ┴ ┴ └──┘
doc └─────┘
66 eq_univ_of_forall $ λ x, begin
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
st └─────
67 rw mem_closure_iff,
id └─────────────┘
src └─┘└─────────────┘
typ └─┘└─────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────┘└─
68 intros U U_op x_in_U,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ─────────────────────┘└─
69 let V := quotient.mk ⁻¹' U,
id └─────────┘ └─┘ ┴
src └───────┘└─────────┘┴└─┘┴
typ └───────┘└─────────┘┴└─┘┴┴
doc └───────┘ ┴└─┘┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴
st ───────────────────────────┘└─
70 cases quotient.exists_rep x with y y_x,
id └─────────────────┘ ┴
src └────┘└─────────────────┘┴ └─────────┘
typ └────┘└─────────────────┘┴┴└─────────┘
doc └────┘ ┴ └─────────┘
txt └────┘ ┴ └─────────┘
par └────┘ ┴ └─────────┘
pid ┴ ┴ └─────────┘
st ───────────────────────────────────────┘└─
71 have y_in_V : y ∈ V, by simp only [mem_preimage, y_x, x_in_U],
id ┴ ┴ ┴ └──────────┘ └─┘ └────┘
src └────────────┘ ┴┴┴ └─────────┘└──────────┘└┘ └┘ ┴
typ └────────────┘┴┴┴┴┴ └─────────┘└──────────┘└┘└─┘└┘└────┘┴
doc └────────────┘ ┴ ┴ └─────────┘ └┘ └┘ ┴
txt └────────────┘ ┴ ┴ └─────────┘ └┘ └┘ ┴
par └────────────┘ ┴ ┴ └─────────┘ └┘ └┘ ┴
pid └─────────┘└─┘ ┴ ┴ ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────┘ └─
72 have V_op : is_open V := U_op,
id └─────┘ ┴ └──┘
src └──────────┘└─────┘┴ └──┘
typ └──────────┘└─────┘┴┴└──┘└──┘
doc └──────────┘└─────┘┴ └──┘
txt └──────────┘ ┴ └──┘
par └──────────┘ ┴ └──┘
pid └───────┘└─┘ ┴ └──┘
st ──────────────────────────────┘└─
73 obtain ⟨w, w_in_V, w_in_range⟩ : (V ∩ s).nonempty := mem_closure_iff.1 (H y) V V_op y_in_V,
id ┴ ┴ └─────────────┘ ┴ ┴ ┴ └──┘ └────┘
src └───────────────────────────────┘ ┴┴┴ └────────────┘└─────────────┘└─┘ ┴ └┘ ┴ ┴
typ └───────────────────────────────┘ ┴┴┴┴└────────────┘└─────────────┘└─┘ ┴┴┴└┘┴┴└──┘┴└────┘
doc └───────────────────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └┘ ┴ ┴
txt └───────────────────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └┘ ┴ ┴
par └───────────────────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └┘ ┴ ┴
pid └─────────────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
74 exact ⟨_, w_in_V, mem_image_of_mem quotient.mk w_in_range⟩
id └────┘ └──────────────┘ └─────────┘ └────────┘
src └────┘ └─┘ └┘└──────────────┘┴└─────────┘┴ └┘
typ └────┘ └─┘└────┘└┘└──────────────┘┴└─────────┘┴└────────┘└┘
doc └────┘ └─┘ └┘ ┴ ┴ └┘
txt └────┘ └─┘ └┘ ┴ ┴ └┘
par └────┘ └─┘ └┘ ┴ ┴ └┘
pid ┴ └─┘ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────┘
75 end
st └─┘
76
77 instance {p : α → Prop} [topological_space α] [discrete_topology α] :
id ┴ └───────────────┘ ┴ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ ┴ └───────────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘
78 discrete_topology (subtype p) :=
id └───────────────┘ └─────┘ ┴
src └───────────────┘ └─────┘
typ └───────────────┘ └─────┘ ┴
doc └───────────────┘
79 ⟨bot_unique $ assume s hs,
id └────────┘ ┴ └┘
src └────────┘
typ └────────┘ ┴ └┘
80 ⟨subtype.val '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.val_injective)⟩⟩
id └─────────┘ └┘ ┴ └──────────────┘ └───────────────────┘ └───────────────────┘
src └─────────┘ └┘ └──────────────┘ └───────────────────┘ └───────────────────┘
typ └─────────┘ └┘ ┴ └──────────────┘ └───────────────────┘ └───────────────────┘
81
82 instance sum.discrete_topology [topological_space α] [topological_space β]
id └───────────────┘ ┴ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘
83 [hα : discrete_topology α] [hβ : discrete_topology β] : discrete_topology (α ⊕ β) :=
id └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘ └───────────────┘ └───────────────┘ ┴
typ └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘ └───────────────┘ └───────────────┘
84 ⟨by unfold sum.topological_space; simp [hα.eq_bot, hβ.eq_bot]⟩
src └──────────────────────────┘ └────┘ └┘ ┴
typ └──────────────────────────┘ └────┘└───────┘└┘└───────┘┴
doc └──────────────────────────┘ └────┘ └┘ ┴
txt └──────────────────────────┘ └────┘ └┘ ┴
par └──────────────────────────┘ └────┘ └┘ ┴
pid └────────────────────┘ ┴┴ └┘ ┴
st └────────────────────────────────────────────────────────┘
85
86 instance sigma.discrete_topology {β : α → Type v} [Πa, topological_space (β a)]
id ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘
87 [h : Πa, discrete_topology (β a)] : discrete_topology (sigma β) :=
id ┴ └───────────────┘ ┴ ┴ └───────────────┘ └───┘ ┴
src └───────────────┘ └───────────────┘ └───┘
typ ┴ └───────────────┘ ┴ ┴ └───────────────┘ └───┘ ┴
doc └───────────────┘ └───────────────┘
88 ⟨by { unfold sigma.topological_space, simp [λ a, (h a).eq_bot] }⟩
id ┴
src └────────────────────────────┘ └────┘ └──┘ ┴ └────────┘
typ └────────────────────────────┘ └────┘ └──┘ ┴┴ └────────┘
doc └────────────────────────────┘ └────┘ └──┘ ┴ └────────┘
txt └────────────────────────────┘ └────┘ └──┘ ┴ └────────┘
par └────────────────────────────┘ └────┘ └──┘ ┴ └────────┘
pid └──────────────────────┘ ┴┴ └──┘ ┴ └───────┘┴
st └───────────────────────────────┘└─────────────────────────┘└┘
89
90 section topα
91
92 variable [topological_space α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
93
94 /-
95 The 𝓝 filter and the subspace topology.
96 -/
97
98 theorem mem_nhds_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
id └─┘ ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ ┴
typ └─┘ ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴
99 t ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 a.val, (@subtype.val α s) ⁻¹' u ⊆ t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──┘┴ └─────────┘ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc ┴ ┴ └─┘
100 mem_nhds_induced subtype.val a t
id └──────────────┘ └─────────┘ ┴ ┴
src └──────────────┘ └─────────┘
typ └──────────────┘ └─────────┘ ┴ ┴
101
102 theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
id └─┘ ┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴┴ ┴ ┴ ┴
103 𝓝 a = comap subtype.val (𝓝 a.val) :=
id ┴ ┴ ┴ └───┘ └─────────┘ ┴ ┴└──┘
src ┴ ┴ └───┘ └─────────┘ ┴ └──┘
typ ┴ ┴ ┴ └───┘ └─────────┘ ┴ ┴└──┘
doc ┴ └───┘ ┴
104 nhds_induced subtype.val a
id └──────────┘ └─────────┘ ┴
src └──────────┘ └─────────┘
typ └──────────┘ └─────────┘ ┴
105
106 end topα
107
108 end constructions
109
110
111 section prod
112 open topological_space
113 variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
id └───────────────┘ └───────────────┘ └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘ └───────────────┘ └───────────────┘
114
115 lemma continuous_fst : continuous (@prod.fst α β) :=
id └────────┘ └──────┘ ┴ ┴
src └────────┘ └──────┘
typ └────────┘ └──────┘ ┴ ┴
doc └────────┘
116 continuous_inf_dom_left continuous_induced_dom
id └─────────────────────┘ └────────────────────┘
src └─────────────────────┘ └────────────────────┘
typ └─────────────────────┘ └────────────────────┘
117
118 lemma continuous_snd : continuous (@prod.snd α β) :=
id └────────┘ └──────┘ ┴ ┴
src └────────┘ └──────┘
typ └────────┘ └──────┘ ┴ ┴
doc └────────┘
119 continuous_inf_dom_right continuous_induced_dom
id └──────────────────────┘ └────────────────────┘
src └──────────────────────┘ └────────────────────┘
typ └──────────────────────┘ └────────────────────┘
120
121 lemma continuous.prod_mk {f : γ → α} {g : γ → β}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
122 (hf : continuous f) (hg : continuous g) : continuous (λx, prod.mk (f x) (g x)) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ └─────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
123 continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
id └────────────────┘ └────────────────────┘ └┘ └────────────────────┘ └┘
src └────────────────┘ └────────────────────┘ └────────────────────┘
typ └────────────────┘ └────────────────────┘ └┘ └────────────────────┘ └┘
124
125 lemma continuous_swap : continuous (prod.swap : α × β → β × α) :=
id └────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───────┘ ┴ ┴
typ └────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └───────┘
126 continuous.prod_mk continuous_snd continuous_fst
id └────────────────┘ └────────────┘ └────────────┘
src └────────────────┘ └────────────┘ └────────────┘
typ └────────────────┘ └────────────┘ └────────────┘
127
128 lemma is_open_prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
id └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─────┘ ┴
src └─┘ └─┘ └─────┘ └─────┘
typ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
129 is_open (set.prod s t) :=
id └─────┘ └──────┘ ┴ ┴
src └─────┘ └──────┘
typ └─────┘ └──────┘ ┴ ┴
doc └─────┘ └──────┘
130 is_open_inter (continuous_fst s hs) (continuous_snd t ht)
id └───────────┘ └────────────┘ ┴ └┘ └────────────┘ ┴ └┘
src └───────────┘ └────────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴ └┘ └────────────┘ ┴ └┘
131
132 lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = filter.prod (𝓝 a) (𝓝 b) :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────────┘ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc ┴ └─────────┘ ┴ ┴
133 by rw [filter.prod, prod.topological_space, nhds_inf, nhds_induced, nhds_induced]
id └─────────┘ └────────────────────┘ └──────┘ └──────────┘ └──────────┘
src └──┘└─────────┘└┘└────────────────────┘└┘└──────┘└┘└──────────┘└┘└──────────┘└─
typ └──┘└─────────┘└┘└────────────────────┘└┘└──────┘└┘└──────────┘└┘└──────────┘└─
doc └──┘└─────────┘└┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ ┴└
st └──────────────┘└──────────────────────┘└────────┘└────────────┘└────────────┘┴└
134
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
135 instance [discrete_topology α] [discrete_topology β] : discrete_topology (α × β) :=
id └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘ └───────────────┘ └───────────────┘ ┴
typ └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘ └───────────────┘ └───────────────┘
136 ⟨eq_of_nhds_eq_nhds $ assume ⟨a, b⟩,
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
137 by rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, nhds_bot, filter.prod_pure_pure]⟩
id └──────────┘ └───────────┘ ┴ └───────────┘ ┴ └──────┘ └───────────────────┘
src └──┘└──────────┘└┘└───────────┘┴ └┘└───────────┘┴ └┘└──────┘└┘└───────────────────┘┴
typ └──┘└──────────┘└┘└───────────┘┴┴└┘└───────────┘┴┴└┘└──────┘└┘└───────────────────┘┴
doc └──┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴
txt └──┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴
par └──┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴
pid └┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴
st └───────────────┘└───────────────┘└───────────────┘└────────┘└─────────────────────┘┴
138
139 lemma prod_mem_nhds_sets {s : set α} {t : set β} {a : α} {b : β}
id └─┘ ┴ └─┘ ┴ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴
140 (ha : s ∈ 𝓝 a) (hb : t ∈ 𝓝 b) : set.prod s t ∈ 𝓝 (a, b) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ ┴
doc ┴ ┴ └──────┘ ┴
141 by rw [nhds_prod_eq]; exact prod_mem_prod ha hb
id └──────────┘ └───────────┘ └┘ └┘
src └──┘└──────────┘┴ └────┘└───────────┘┴ ┴ └
typ └──┘└──────────┘┴ └────┘└───────────┘┴└┘┴└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └
txt └──┘ ┴ └────┘ ┴ ┴ └
par └──┘ ┴ └────┘ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st └───────────────┘┴└───────────────────────────
142
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
143 lemma nhds_swap (a : α) (b : β) : 𝓝 (a, b) = (𝓝 (b, a)).map prod.swap :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ └───────┘
src ┴ ┴ ┴ ┴ ┴ └─┘ └───────┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ └───────┘
doc ┴ ┴ └─┘ └───────┘
144 by rw [nhds_prod_eq, filter.prod_comm, nhds_prod_eq]; refl
id └──────────┘ └──────────────┘ └──────────┘
src └──┘└──────────┘└┘└──────────────┘└┘└──────────┘┴ └────
typ └──┘└──────────┘└┘└──────────────┘└┘└──────────┘┴ └────
doc └──┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └
st └───────────────┘└────────────────┘└────────────┘┴└──────
145
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
146 lemma tendsto_prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β}
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
147 (ha : tendsto ma f (𝓝 a)) (hb : tendsto mb f (𝓝 b)) :
id └─────┘ └┘ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴
typ └─────┘ └┘ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
148 tendsto (λc, (ma c, mb c)) f (𝓝 (a, b)) :=
id └─────┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴
doc └─────┘ ┴
149 by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
id └──────────┘ └────────────────────┘ └┘ └┘
src └──┘└──────────┘┴ └────┘└────────────────────┘┴ ┴ └
typ └──┘└──────────┘┴ └────┘└────────────────────┘┴└┘┴└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └
txt └──┘ ┴ └────┘ ┴ ┴ └
par └──┘ ┴ └────┘ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st └───────────────┘┴└────────────────────────────────────
150
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
151 lemma continuous_at.prod {f : α → β} {g : α → γ} {x : α}
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
152 (hf : continuous_at f x) (hg : continuous_at g x) : continuous_at (λx, (f x, g x)) x :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
153 tendsto_prod_mk_nhds hf hg
id └──────────────────┘ └┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘ └┘
154
155 lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (set α)} {t : set (set β)}
id └─┘ └─┘ ┴ └─┘ └─┘ ┴
src └─┘ └─┘ └─┘ └─┘
typ └─┘ └─┘ ┴ └─┘ └─┘ ┴
156 (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
id └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘
src └┘ ┴ └──┘ └┘ ┴ └──┘
typ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘
157 @prod.topological_space α β (generate_from s) (generate_from t) =
id └────────────────────┘ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴
src └────────────────────┘ └───────────┘ └───────────┘ ┴
typ └────────────────────┘ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴
doc └───────────┘ └───────────┘
158 generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} :=
id └───────────┘ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └───────────┘ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
doc └───────────┘ └──────┘
159 let G := generate_from {g | ∃u∈s, ∃v∈t, g = set.prod u v} in
id ┴ └───────────┘ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ └───────────┘ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴
doc └───────────┘ └──────┘
160 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
161 (le_generate_from $ assume g ⟨u, hu, v, hv, g_eq⟩, g_eq.symm ▸
id └──────────────┘ ┴ ┴ └┘ └┘ └──┘ └───┘ ┴
src └──────────────┘ └───┘ ┴
typ └──────────────┘ ┴ ┴ └┘ └┘ └──┘ └───┘ ┴
162 @is_open_prod _ _ (generate_from s) (generate_from t) _ _
id └──────────┘ └───────────┘ ┴ └───────────┘ ┴
src └──────────┘ └───────────┘ └───────────┘
typ └──────────┘ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
163 (generate_open.basic _ hu) (generate_open.basic _ hv))
id └─────────────────┘ └─────────────────┘
src └─────────────────┘ └─────────────────┘
typ └─────────────────┘ └─────────────────┘
164 (le_inf
id └────┘
src └────┘
typ └────┘
165 (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume u hu,
id └─────────────────────────┘└─┘ └──────────────┘ ┴ └┘
src └─────────────────────────┘└─┘ └──────────────┘
typ └─────────────────────────┘└─┘ └──────────────┘ ┴ └┘
166 have (⋃v∈t, set.prod u v) = prod.fst ⁻¹' u,
id ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴
src ┴ ┴ └──────┘ ┴ └──────┘ └─┘
typ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴
doc ┴ ┴ └──────┘ └─┘
167 from calc (⋃v∈t, set.prod u v) = set.prod u univ :
id ┴┴ ┴┴ └──────┘ ┴ ┴ └──────┘ ┴ └──┘
src ┴ ┴ └──────┘ └──────┘ └──┘
typ ┴┴ ┴┴ └──────┘ ┴ ┴ └──────┘ ┴ └──┘
doc ┴ ┴ └──────┘ └──────┘
168 set.ext $ assume ⟨a, b⟩, by rw ← ht; simp [and.left_comm] {contextual:=tt}
id └─────┘ ┴ └┘ └───────────┘ └┘
src └─────┘ └───┘ └────┘└───────────┘└┘ └──────────┘└┘└─
typ └─────┘ ┴ └───┘└┘ └────┘└───────────┘└┘ └──────────┘└┘└─
doc └───┘ └────┘ └┘ └──────────┘ └─
txt └───┘ └────┘ └┘ └──────────┘ └─
par └───┘ └────┘ └┘ └──────────┘ └─
pid └─┘ ┴┴ ┴┴ └──────────┘ ┴└
st └───────────────────────────────────────────────
169 ... = prod.fst ⁻¹' u : by simp [set.prod, preimage],
id └──────┘ └─┘ ┴ └──────┘ └──────┘
src ─────────┘ └──────┘ └─┘ └────┘└──────┘└┘└──────┘┴
typ ─────────┘ └──────┘ └─┘ ┴ └────┘└──────┘└┘└──────┘┴
doc ─────────┘ └─┘ └────┘└──────┘└┘└──────┘┴
txt ─────────┘ └────┘ └┘ ┴
par ─────────┘ └────┘ └┘ ┴
pid ─────────┘ ┴┴ └┘ ┴
st ─────────┘ └────────────────────────┘
170 show G.is_open (prod.fst ⁻¹' u),
id ┴└──────┘ └──────┘ └─┘ ┴
src └──────┘ └──────┘ └─┘
typ ┴└──────┘ └──────┘ └─┘ ┴
doc └─┘
171 from this ▸ @is_open_Union _ _ G _ $ assume v, @is_open_Union _ _ G _ $ assume hv,
id └──┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └┘
src ┴ └───────────┘ └───────────┘
typ └──┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └┘
172 generate_open.basic _ ⟨_, hu, _, hv, rfl⟩)
id └─────────────────┘ └┘ └┘ └─┘
src └─────────────────┘ └─┘
typ └─────────────────┘ └┘ └┘ └─┘
173 (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume v hv,
id └─────────────────────────┘└─┘ └──────────────┘ ┴ └┘
src └─────────────────────────┘└─┘ └──────────────┘
typ └─────────────────────────┘└─┘ └──────────────┘ ┴ └┘
174 have (⋃u∈s, set.prod u v) = prod.snd ⁻¹' v,
id ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴
src ┴ ┴ └──────┘ ┴ └──────┘ └─┘
typ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴
doc ┴ ┴ └──────┘ └─┘
175 from calc (⋃u∈s, set.prod u v) = set.prod univ v:
id ┴┴ ┴┴ └──────┘ ┴ ┴ └──────┘ └──┘ ┴
src ┴ ┴ └──────┘ └──────┘ └──┘
typ ┴┴ ┴┴ └──────┘ ┴ ┴ └──────┘ └──┘ ┴
doc ┴ ┴ └──────┘ └──────┘
176 set.ext $ assume ⟨a, b⟩, by rw [←hs]; by_cases b ∈ v; simp [h] {contextual:=tt}
id └─────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
src └─────┘ └───┘ ┴ └───────┘ ┴┴┴ └────┘ └┘ └──────────┘└┘└─
typ └─────┘ ┴ └───┘└┘┴ └───────┘┴┴┴┴┴ └────┘┴└┘ └──────────┘└┘└─
doc └───┘ ┴ └───────┘ ┴ ┴ └────┘ └┘ └──────────┘ └─
txt └───┘ ┴ └───────┘ ┴ ┴ └────┘ └┘ └──────────┘ └─
par └───┘ ┴ └───────┘ ┴ ┴ └────┘ └┘ └──────────┘ └─
pid └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──────────┘ ┴└
st └──────┘┴└───────────────────────────────────────────
177 ... = prod.snd ⁻¹' v : by simp [set.prod, preimage],
id └──────┘ └─┘ ┴ └──────┘ └──────┘
src ─────────┘ └──────┘ └─┘ └────┘└──────┘└┘└──────┘┴
typ ─────────┘ └──────┘ └─┘ ┴ └────┘└──────┘└┘└──────┘┴
doc ─────────┘ └─┘ └────┘└──────┘└┘└──────┘┴
txt ─────────┘ └────┘ └┘ ┴
par ─────────┘ └────┘ └┘ ┴
pid ─────────┘ ┴┴ └┘ ┴
st ─────────┘ └────────────────────────┘
178 show G.is_open (prod.snd ⁻¹' v),
id ┴└──────┘ └──────┘ └─┘ ┴
src └──────┘ └──────┘ └─┘
typ ┴└──────┘ └──────┘ └─┘ ┴
doc └─┘
179 from this ▸ @is_open_Union _ _ G _ $ assume u, @is_open_Union _ _ G _ $ assume hu,
id └──┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └┘
src ┴ └───────────┘ └───────────┘
typ └──┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └┘
180 generate_open.basic _ ⟨_, hu, _, hv, rfl⟩))
id └─────────────────┘ └┘ └┘ └─┘
src └─────────────────┘ └─┘
typ └─────────────────┘ └┘ └┘ └─┘
181
182 lemma prod_eq_generate_from :
183 prod.topological_space =
id └────────────────────┘ ┴
src └────────────────────┘ ┴
typ └────────────────────┘ ┴
184 generate_from {g | ∃(s:set α) (t:set β), is_open s ∧ is_open t ∧ g = set.prod s t} :=
id └───────────┘ ┴┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └───────────┘ ┴ ┴ └─┘ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └──────┘
typ └───────────┘ ┴┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └───────────┘ └─────┘ └─────┘ └──────┘
185 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
186 (le_generate_from $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ is_open_prod hs ht)
id └──────────────┘ ┴ ┴ └┘ └┘ └──┘ └───┘ ┴ └──────────┘
src └──────────────┘ └───┘ ┴ └──────────┘
typ └──────────────┘ ┴ ┴ └┘ └┘ └──┘ └───┘ ┴ └──────────┘
187 (le_inf
id └────┘
src └────┘
typ └────┘
188 (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨t, univ, by simpa [set.prod_eq] using ht⟩)
id └────────────────┘ ┴ └┘ └─────────────────┘ ┴ └──┘ └─────────┘ └┘
src └────────────────┘ └─────────────────┘ └──┘ └─────┘└─────────┘└──────┘
typ └────────────────┘ ┴ └┘ └─────────────────┘ ┴ └──┘ └─────┘└─────────┘└──────┘└┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────┘
189 (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨univ, t, by simpa [set.prod_eq] using ht⟩))
id └────────────────┘ ┴ └┘ └─────────────────┘ └──┘ ┴ └─────────┘ └┘
src └────────────────┘ └─────────────────┘ └──┘ └─────┘└─────────┘└──────┘
typ └────────────────┘ ┴ └┘ └─────────────────┘ └──┘ ┴ └─────┘└─────────┘└──────┘└┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────┘
190
191 lemma is_open_prod_iff {s : set (α×β)} : is_open s ↔
id └─┘ ┴┴┴ └─────┘ ┴ ┴
src └─┘ ┴ └─────┘ ┴
typ └─┘ ┴┴┴ └─────┘ ┴ ┴
doc └─────┘
192 (∀a b, (a, b) ∈ s → ∃u v, is_open u ∧ is_open v ∧ a ∈ u ∧ b ∈ v ∧ set.prod u v ⊆ s) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └──────┘
193 begin
st └─────
194 rw [is_open_iff_nhds],
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────┘└──
195 simp [nhds_prod_eq, mem_prod_iff],
id └──────────┘ └──────────┘
src └────┘└──────────┘└┘└──────────┘┴
typ └────┘└──────────┘└┘└──────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ──────────────────────────────────┘└─
196 simp [mem_nhds_sets_iff],
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────────────┘└─
197 exact forall_congr (assume a, ball_congr $ assume b h,
id └──────────┘ └────────┘
src └────┘└──────────┘┴ └──┘└────────┘┴ ┴ └─────
typ └────┘└──────────┘┴ └──┘└────────┘┴ ┴ └─────
doc └────┘ ┴ └──┘ ┴ ┴ └─────
txt └────┘ ┴ └──┘ ┴ ┴ └─────
par └────┘ ┴ └──┘ ┴ ┴ └─────
pid ┴ ┴ └──┘ ┴ ┴ └─────
st ─────────────────────────────────────────────────────────
198 ⟨assume ⟨u', ⟨u, us, uo, au⟩, v', ⟨v, vs, vo, bv⟩, h⟩,
id ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
src ───┘ └┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └──
typ ───┘ └┘ └┘ ┴└┘└┘└┘└┘└┘└┘└─┘ └┘ ┴└┘└┘└┘└┘└┘└┘└─┘┴└──
doc ───┘ └┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └──
txt ───┘ └┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └──
par ───┘ └┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └──
pid ───┘ └┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └──
st ───────────────────────────────────────────────────────────
199 ⟨u, uo, v, vo, au, bv, subset.trans (set.prod_mono us vs) h⟩,
id └──────────┘ └───────────┘
src ─────┘ └┘ └┘ └┘ └┘ └┘ └┘└──────────┘┴ └───────────┘┴ ┴ └┘ └──
typ ─────┘ └┘ └┘ └┘ └┘ └┘ └┘└──────────┘┴ └───────────┘┴ ┴ └┘ └──
doc ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └┘ └──
txt ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └┘ └──
par ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └┘ └──
pid ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └┘ └──
st ────────────────────────────────────────────────────────────────────
200 assume ⟨u, uo, v, vo, au, bv, h⟩,
id ┴ └┘ ┴ └┘ └┘ └┘ ┴
src ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └──
typ ─────┘ └┘┴└┘└┘└┘┴└┘└┘└┘└┘└┘└┘└┘┴└──
doc ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └──
txt ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └──
par ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └──
pid ─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └──
st ────────────────────────────────────────
201 ⟨u, ⟨u, subset.refl u, uo, au⟩, v, ⟨v, subset.refl v, vo, bv⟩, h⟩⟩)
id └─────────┘
src ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘└─────────┘┴ └┘ └┘ └─┘ └──┘
typ ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘└─────────┘┴ └┘ └┘ └─┘ └──┘
doc ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘ ┴ └┘ └┘ └─┘ └──┘
txt ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘ ┴ └┘ └┘ └─┘ └──┘
par ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘ ┴ └┘ └┘ └─┘ └──┘
pid ─────┘ └┘ └┘ ┴ └┘ └┘ └─┘ └┘ └┘ ┴ └┘ └┘ └─┘ └─┘┴
st ─────────────────────────────────────────────────────────────────────────┘
202 end
st └─┘
203
204 /-- The first projection in a product of topological spaces sends open sets to open sets. -/
205 lemma is_open_map_fst : is_open_map (@prod.fst α β) :=
id └─────────┘ └──────┘ ┴ ┴
src └─────────┘ └──────┘
typ └─────────┘ └──────┘ ┴ ┴
doc └─────────┘
206 begin
st └─────
207 assume s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
208 rw is_open_iff_forall_mem_open,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────────┘└─
209 assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
210 rw mem_image_eq at xs,
id └──────────┘
src └─┘└──────────┘└────┘
typ └─┘└──────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ──────────────────────┘└─
211 rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
id └┘
src └─────┘ └──────────────────────┘
typ └─────┘└┘└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ──────────────────────────────────┘└─
212 rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
id └──────────────┘ └┘ └┘
src └─────┘└──────────────┘└─┘ └───┘ └────────────────────────────────────────────┘
typ └─────┘└──────────────┘└─┘└┘└───┘└┘└────────────────────────────────────────────┘
doc └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
txt └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
par └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
pid ┴ └─┘ └───┘ └────────────────────────────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
213 simp at yx,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────┘└─
214 rw yx at yo₁,
id └┘
src └─┘ └─────┘
typ └─┘└┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────┘└─
215 refine ⟨o₁, _, o₁_open, yo₁⟩,
id └┘ └─────┘ └─┘
src └─────┘ └───┘ └┘ ┴
typ └─────┘ └┘└───┘└─────┘└┘└─┘┴
doc └─────┘ └───┘ └┘ ┴
txt └─────┘ └───┘ └┘ ┴
par └─────┘ └───┘ └┘ ┴
pid ┴ └───┘ └┘ ┴
st ─────────────────────────────┘└─
216 assume z zs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
217 rw mem_image_eq,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
218 exact ⟨(z, y₂), ho (by simp [zs, yo₂]), rfl⟩
id ┴ └┘ └┘ └┘ └─┘ └─┘
src └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘└─┘└┘
typ └────┘ ┴└┘└┘└─┘└┘┴ ┴└────┘└┘└┘└─┘┴└─┘└─┘└┘
doc └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
txt └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
par └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
pid ┴ └┘ └─┘ ┴ └─────┘ └┘ └──┘ ┴┴
st ───────────────────────┘└─────────────┘└──────┘
219 end
st └─┘
220
221 /-- The second projection in a product of topological spaces sends open sets to open sets. -/
222 lemma is_open_map_snd : is_open_map (@prod.snd α β) :=
id └─────────┘ └──────┘ ┴ ┴
src └─────────┘ └──────┘
typ └─────────┘ └──────┘ ┴ ┴
doc └─────────┘
223 begin
st └─────
224 /- This lemma could be proved by composing the fact that the first projection is open, and
st ─────────────────────────────────────────────────────────────────────────────────────────────
225 exchanging coordinates is a homeomorphism, hence open. As the `prod_comm` homeomorphism is defined
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
226 later, we rather go for the direct proof, copy-pasting the proof for the first projection. -/
st ────────────────────────────────────────────────────────────────────────────────────────────────
227 assume s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
228 rw is_open_iff_forall_mem_open,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────────┘└─
229 assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
230 rw mem_image_eq at xs,
id └──────────┘
src └─┘└──────────┘└────┘
typ └─┘└──────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ──────────────────────┘└─
231 rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
id └┘
src └─────┘ └──────────────────────┘
typ └─────┘└┘└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ──────────────────────────────────┘└─
232 rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
id └──────────────┘ └┘ └┘
src └─────┘└──────────────┘└─┘ └───┘ └────────────────────────────────────────────┘
typ └─────┘└──────────────┘└─┘└┘└───┘└┘└────────────────────────────────────────────┘
doc └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
txt └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
par └─────┘ └─┘ └───┘ └────────────────────────────────────────────┘
pid ┴ └─┘ └───┘ └────────────────────────────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
233 simp at yx,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────┘└─
234 rw yx at yo₂,
id └┘
src └─┘ └─────┘
typ └─┘└┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────┘└─
235 refine ⟨o₂, _, o₂_open, yo₂⟩,
id └┘ └─────┘ └─┘
src └─────┘ └───┘ └┘ ┴
typ └─────┘ └┘└───┘└─────┘└┘└─┘┴
doc └─────┘ └───┘ └┘ ┴
txt └─────┘ └───┘ └┘ ┴
par └─────┘ └───┘ └┘ ┴
pid ┴ └───┘ └┘ ┴
st ─────────────────────────────┘└─
236 assume z zs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
237 rw mem_image_eq,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
238 exact ⟨(y₁, z), ho (by simp [zs, yo₁]), rfl⟩
id └┘ ┴ └┘ └┘ └─┘ └─┘
src └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘└─┘└┘
typ └────┘ └┘└┘┴└─┘└┘┴ ┴└────┘└┘└┘└─┘┴└─┘└─┘└┘
doc └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
txt └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
par └────┘ └┘ └─┘ ┴ ┴└────┘ └┘ ┴└─┘ └┘
pid ┴ └┘ └─┘ ┴ └─────┘ └┘ └──┘ ┴┴
st ───────────────────────┘└─────────────┘└──────┘
239 end
st └─┘
240
241 /-- A product set is open in a product space if and only if each factor is open, or one of them is
242 empty -/
243 lemma is_open_prod_iff' {s : set α} {t : set β} :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
244 is_open (set.prod s t) ↔ (is_open s ∧ is_open t) ∨ (s = ∅) ∨ (t = ∅) :=
id └─────┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──────┘ └─────┘ └─────┘
245 begin
st └─────
246 cases (set.prod s t).eq_empty_or_nonempty with h h,
id └──────┘ ┴ ┴
src └────┘ └──────┘┴ ┴ └─────────────────────────────┘
typ └────┘ └──────┘┴┴┴┴└─────────────────────────────┘
doc └────┘ └──────┘┴ ┴ └─────────────────────────────┘
txt └────┘ ┴ ┴ └─────────────────────────────┘
par └────┘ ┴ ┴ └─────────────────────────────┘
pid ┴ ┴ ┴ └───────────────────┘└────────┘
st ───────────────────────────────────────────────────┘└─
247 { simp [h, prod_eq_empty_iff.1 h] },
id ┴ └───────────────┘ ┴
src └────┘ └┘└───────────────┘└─┘ └┘
typ └────┘┴└┘└───────────────┘└─┘┴└┘
doc └────┘ └┘ └─┘ └┘
txt └────┘ └┘ └─┘ └┘
par └────┘ └┘ └─┘ └┘
pid ┴┴ └┘ └─┘ ┴┴
st ───┘└──────────────────────────────┘└┘└
248 { have st : s.nonempty ∧ t.nonempty, from prod_nonempty_iff.1 h,
id └────────┘ └────────┘ └───────────────┘ ┴
src └────────┘└────────┘┴ ┴└────────┘ └───┘└───────────────┘└─┘
typ └────────┘└────────┘┴ ┴└────────┘ └───┘└───────────────┘└─┘┴
doc └────────┘└────────┘┴ ┴└────────┘ └───┘ └─┘
txt └────────┘ ┴ ┴ └───┘ └─┘
par └────────┘ ┴ ┴ └───┘ └─┘
pid └─────┘└─┘ ┴ ┴ └───┘ └─┘
st ────────────────────────────────────┘└──────────────────────────┘└─
249 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
250 { assume H : is_open (set.prod s t),
id └─────┘ └──────┘ ┴ ┴
src └─────────┘└─────┘┴ └──────┘┴ ┴ ┴
typ └─────────┘└─────┘┴ └──────┘┴┴┴┴┴
doc └─────────┘└─────┘┴ └──────┘┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴
pid └─────────┘ ┴ ┴ ┴ ┴
st ─────┘└───────────────────────────────┘└─
251 refine or.inl ⟨_, _⟩,
id └────┘
src └─────┘└────┘┴ └───┘
typ └─────┘└────┘┴ └───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────┘└─
252 show is_open s,
id └─────┘ ┴
src └───┘└─────┘┴
typ └───┘└─────┘┴┴
doc └───┘└─────┘┴
txt └───┘ ┴
par └───┘ ┴
pid └───┘ ┴
st ──────────────────────
253 { rw ← fst_image_prod s st.2,
id └────────────┘ ┴ └┘
src └───┘└────────────┘┴ ┴ └┘
typ └───┘└────────────┘┴┴┴└┘└┘
doc └───┘ ┴ ┴ └┘
txt └───┘ ┴ ┴ └┘
par └───┘ ┴ ┴ └┘
pid └─┘ ┴ ┴ └┘
st ───────┘└────────────────────────┘└─
254 exact is_open_map_fst _ H },
id └─────────────┘ ┴
src └────┘└─────────────┘└─┘ ┴
typ └────┘└─────────────┘└─┘┴┴
doc └────┘└─────────────┘└─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────┘└┘└
255 show is_open t,
id └─────┘ ┴
src └───┘└─────┘┴
typ └───┘└─────┘┴┴
doc └───┘└─────┘┴
txt └───┘ ┴
par └───┘ ┴
pid └───┘ ┴
st ──────────────────────
256 { rw ← snd_image_prod st.1 t,
id └────────────┘ └┘ ┴
src └───┘└────────────┘┴ └─┘
typ └───┘└────────────┘┴└┘└─┘┴
doc └───┘ ┴ └─┘
txt └───┘ ┴ └─┘
par └───┘ ┴ └─┘
pid └─┘ ┴ └─┘
st ─────────────────────────────────┘└─
257 exact is_open_map_snd _ H } },
id └─────────────┘ ┴
src └────┘└─────────────┘└─┘ ┴
typ └────┘└─────────────┘└─┘┴┴
doc └────┘└─────────────┘└─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────┘└──┘└
258 { assume H,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
259 simp [st.1.ne_empty, st.2.ne_empty] at H,
id └┘ └┘
src └────┘ └───────────┘ └───────────────┘
typ └────┘└┘└───────────┘└┘└───────────────┘
doc └────┘ └───────────┘ └───────────────┘
txt └────┘ └───────────┘ └───────────────┘
par └────┘ └───────────┘ └───────────────┘
pid ┴┴ └───────────┘ └──────────┘┴└──┘
st ─────────────────────────────────────────────┘└─
260 exact is_open_prod H.1 H.2 } }
id └──────────┘ ┴
src └────┘└──────────┘┴ └─┘ └─┘
typ └────┘└──────────┘┴ └─┘┴└─┘
doc └────┘ ┴ └─┘ └─┘
txt └────┘ ┴ └─┘ └─┘
par └────┘ ┴ └─┘ └─┘
pid ┴ ┴ └─┘ └─┘
st ────────────────────────────────┘└───
261 end
st ──┘
262
263 lemma closure_prod_eq {s : set α} {t : set β} :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
264 closure (set.prod s t) = set.prod (closure s) (closure t) :=
id └─────┘ └──────┘ ┴ ┴ ┴ └──────┘ └─────┘ ┴ └─────┘ ┴
src └─────┘ └──────┘ ┴ └──────┘ └─────┘ └─────┘
typ └─────┘ └──────┘ ┴ ┴ ┴ └──────┘ └─────┘ ┴ └─────┘ ┴
doc └─────┘ └──────┘ └──────┘ └─────┘ └─────┘
265 set.ext $ assume ⟨a, b⟩,
id └─────┘ ┴┴ ┴
src └─────┘
typ └─────┘ ┴┴ ┴
266 have filter.prod (𝓝 a) (𝓝 b) ⊓ principal (set.prod s t) =
id └─────────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴
typ └─────────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴ ┴ ┴
doc └─────────┘ ┴ ┴ └───────┘ └──────┘
267 filter.prod (𝓝 a ⊓ principal s) (𝓝 b ⊓ principal t),
id └─────────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴
src └─────────┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘
typ └─────────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴
doc └─────────┘ ┴ └───────┘ ┴ └───────┘
268 by rw [←prod_inf_prod, prod_principal_principal],
id └───────────┘ └──────────────────────┘
src └───┘└───────────┘└┘└──────────────────────┘┴
typ └───┘└───────────┘└┘└──────────────────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └─┘ └┘ ┴
st └─────────────────┘└────────────────────────┘┴
269 by simp [closure_eq_nhds, nhds_prod_eq, this]; exact prod_ne_bot
id └─────────────┘ └──────────┘ └──┘ └─────────┘
src └────┘└─────────────┘└┘└──────────┘└┘ ┴ └────┘└─────────┘└
typ └────┘└─────────────┘└┘└──────────┘└┘└──┘┴ └────┘└─────────┘└
doc └────┘ └┘ └┘ ┴ └────┘ └
txt └────┘ └┘ └┘ ┴ └────┘ └
par └────┘ └┘ └┘ ┴ └────┘ └
pid ┴┴ └┘ └┘ ┴ ┴ └
st └──────────────────────────────────────────────────────────────
270
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
271 lemma mem_closure2 {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β}
id └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
272 (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
id └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
src └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────┘
typ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
doc └────────┘ └─────┘ └─────┘
273 (hu : ∀a b, a ∈ s → b ∈ t → f a b ∈ u) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
274 f a b ∈ closure u :=
id ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
275 have (a, b) ∈ closure (set.prod s t), by rw [closure_prod_eq]; from ⟨ha, hb⟩,
id ┴┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────────────┘ └┘ └┘
src ┴ ┴ └─────┘ └──────┘ └──┘└─────────────┘┴ └───┘ └┘ ┴
typ ┴┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └──┘└─────────────┘┴ └───┘ └┘└┘└┘┴
doc └─────┘ └──────┘ └──┘ ┴ └───┘ └┘ ┴
txt └──┘ ┴ └───┘ └┘ ┴
par └──┘ ┴ └───┘ └┘ ┴
pid └┘ ┴ └───┘ └┘ ┴
st └──────────────────┘┴└─────────────┘
276 show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
id ┴┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴
doc └─────┘
277 mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
id └─────────┘ └┘ └──┘ ┴┴ ┴ ┴└┘ └┘ └┘
src └─────────┘
typ └─────────┘ └┘ └──┘ ┴┴ ┴ ┴└┘ └┘ └┘
278
279 lemma is_closed_prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
id └─┘ ┴ └─┘ ┴ └───────┘ └┘ └───────┘ └┘
src └─┘ └─┘ └───────┘ └───────┘
typ └─┘ ┴ └─┘ ┴ └───────┘ └┘ └───────┘ └┘
doc └───────┘ └───────┘
280 is_closed (set.prod s₁ s₂) :=
id └───────┘ └──────┘ └┘ └┘
src └───────┘ └──────┘
typ └───────┘ └──────┘ └┘ └┘
doc └───────┘ └──────┘
281 closure_eq_iff_is_closed.mp $ by simp [h₁, h₂, closure_prod_eq, closure_eq_of_is_closed]
id └──────────────────────┘└─┘ └┘ └┘ └─────────────┘ └─────────────────────┘
src └──────────────────────┘└─┘ └────┘ └┘ └┘└─────────────┘└┘└─────────────────────┘└─
typ └──────────────────────┘└─┘ └────┘└┘└┘└┘└┘└─────────────┘└┘└─────────────────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────
282
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
283 lemma inducing.prod_mk {f : α → β} {g : γ → δ} (hf : inducing f) (hg : inducing g) :
id ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴
284 inducing (λx:α×γ, (f x.1, g x.2)) :=
id └──────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
src └──────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
285 ⟨by rw [prod.topological_space, prod.topological_space, hf.induced, hg.induced,
id └────────────────────┘ └────────────────────┘
src └──┘└────────────────────┘└┘└────────────────────┘└┘ └┘ └─
typ └──┘└────────────────────┘└┘└────────────────────┘└┘└────────┘└┘└────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st └─────────────────────────┘└──────────────────────┘└──────────┘└──────────┘└─
286 induced_compose, induced_compose, induced_inf, induced_compose, induced_compose]⟩
id └─────────────┘ └─────────────┘ └─────────┘ └─────────────┘ └─────────────┘
src ────────┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────────┘└┘└─────────────┘┴
typ ────────┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────────┘└┘└─────────────┘┴
doc ────────┘ └┘ └┘ └┘ └┘ ┴
txt ────────┘ └┘ └┘ └┘ └┘ ┴
par ────────┘ └┘ └┘ └┘ └┘ ┴
pid ────────┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└───────────────┘└───────────┘└───────────────┘└───────────────┘┴
287
288 lemma embedding.prod_mk {f : α → β} {g : γ → δ} (hf : embedding f) (hg : embedding g) :
id ┴ ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴
src └───────┘ └───────┘
typ ┴ ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴
doc └───────┘ └───────┘
289 embedding (λx:α×γ, (f x.1, g x.2)) :=
id └───────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
doc └───────┘
290 { inj := assume ⟨x₁, x₂⟩ ⟨y₁, y₂⟩, by simp; exact assume h₁ h₂, ⟨hf.inj h₁, hg.inj h₂⟩,
id ┴ ┴ └────┘ └────┘
src └──┘ └────┘ └──────┘ └────┘┴ └┘└────┘┴ ┴
typ ┴ ┴ └──┘ └────┘ └──────┘ └────┘┴ └┘└────┘┴ ┴
doc └──┘ └────┘ └──────┘ ┴ └┘ ┴ ┴
txt └──┘ └────┘ └──────┘ ┴ └┘ ┴ ┴
par └──┘ └────┘ └──────┘ ┴ └┘ ┴ ┴
pid ┴ └──────┘ ┴ └┘ ┴ ┴
st └───────────────────────────────────────────────┘
291 ..hf.to_inducing.prod_mk hg.to_inducing }
id └┘└──────────┘└──────┘ └┘└──────────┘
src └──────────┘└──────┘ └──────────┘
typ └┘└──────────┘└──────┘ └┘└──────────┘
292
293 protected lemma is_open_map.prod {f : α → β} {g : γ → δ} (hf : is_open_map f) (hg : is_open_map g) :
id ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
294 is_open_map (λ p : α × γ, (f p.1, g p.2)) :=
id └─────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴
doc └─────────┘
295 begin
st └─────
296 rw [is_open_map_iff_nhds_le],
id └─────────────────────┘
src └──┘└─────────────────────┘┴
typ └──┘└─────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────────────┘└──
297 rintros ⟨a, b⟩,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └─────┘
st ───────────────┘└─
298 rw [nhds_prod_eq, nhds_prod_eq, ← filter.prod_map_map_eq],
id └──────────┘ └──────────┘ └────────────────────┘
src └──┘└──────────┘└┘└──────────┘└──┘└────────────────────┘┴
typ └──┘└──────────┘└┘└──────────┘└──┘└────────────────────┘┴
doc └──┘ └┘ └──┘ ┴
txt └──┘ └┘ └──┘ ┴
par └──┘ └┘ └──┘ ┴
pid └┘ └┘ └──┘ ┴
st ─────────────────┘└────────────┘└────────────────────────┘└──
299 exact filter.prod_mono (is_open_map_iff_nhds_le.1 hf a) (is_open_map_iff_nhds_le.1 hg b)
id └──────────────┘ └┘ ┴ └─────────────────────┘ └┘ ┴
src └────┘└──────────────┘┴ └─┘ ┴ └┘ └─────────────────────┘└─┘ ┴ └┘
typ └────┘└──────────────┘┴ └─┘└┘┴┴└┘ └─────────────────────┘└─┘└┘┴┴└┘
doc └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘
par └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘
pid ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘
300 end
st └─┘
301
302 protected lemma open_embedding.prod {f : α → β} {g : γ → δ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
303 (hf : open_embedding f) (hg : open_embedding g) : open_embedding (λx:α×γ, (f x.1, g x.2)) :=
id └────────────┘ ┴ └────────────┘ ┴ └────────────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
src └────────────┘ └────────────┘ └────────────┘ ┴ ┴ ┴ ┴
typ └────────────┘ ┴ └────────────┘ ┴ └────────────┘ ┴┴┴ ┴┴ ┴┴ ┴ ┴┴
doc └────────────┘ └────────────┘ └────────────┘
304 open_embedding_of_embedding_open (hf.1.prod_mk hg.1)
id └──────────────────────────────┘ └┘┴ └─────┘ └┘┴
src └──────────────────────────────┘ ┴ └─────┘ ┴
typ └──────────────────────────────┘ └┘┴ └─────┘ └┘┴
305 (hf.is_open_map.prod hg.is_open_map)
id └┘└──────────┘└───┘ └┘└──────────┘
src └──────────┘└───┘ └──────────┘
typ └┘└──────────┘└───┘ └┘└──────────┘
306
307 lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
id ┴ ┴ └────────┘ ┴ └───────┘ ┴ ┴┴ ┴ ┴
src └────────┘ └───────┘ ┴
typ ┴ ┴ └────────┘ ┴ └───────┘ ┴ ┴┴ ┴ ┴
doc └────────┘ └───────┘
308 embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id
id └────────────────────────────┘ └───────────┘└──────┘ └┘ └────────────┘ └──────────┘
src └────────────────────────────┘ └───────────┘└──────┘ └────────────┘ └──────────┘
typ └────────────────────────────┘ └───────────┘└──────┘ └┘ └────────────┘ └──────────┘
309
310 end prod
311
312 section sum
313 variables [topological_space α] [topological_space β] [topological_space γ]
id └───────────────┘ └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘ └───────────────┘
314
315 lemma continuous_inl : continuous (@sum.inl α β) :=
id └────────┘ └─────┘ ┴ ┴
src └────────┘ └─────┘
typ └────────┘ └─────┘ ┴ ┴
doc └────────┘
316 continuous_sup_rng_left continuous_coinduced_rng
id └─────────────────────┘ └──────────────────────┘
src └─────────────────────┘ └──────────────────────┘
typ └─────────────────────┘ └──────────────────────┘
317
318 lemma continuous_inr : continuous (@sum.inr α β) :=
id └────────┘ └─────┘ ┴ ┴
src └────────┘ └─────┘
typ └────────┘ └─────┘ ┴ ┴
doc └────────┘
319 continuous_sup_rng_right continuous_coinduced_rng
id └──────────────────────┘ └──────────────────────┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ └──────────────────────┘
320
321 lemma continuous_sum_rec {f : α → γ} {g : β → γ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
322 (hf : continuous f) (hg : continuous g) : @continuous (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴ └─────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
323 continuous_sup_dom hf hg
id └────────────────┘ └┘ └┘
src └────────────────┘
typ └────────────────┘ └┘ └┘
324
325 lemma embedding_inl : embedding (@sum.inl α β) :=
id └───────┘ └─────┘ ┴ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴ ┴
doc └───────┘
326 { induced := begin
st └─────
327 unfold sum.topological_space,
src └──────────────────────────┘
typ └──────────────────────────┘
doc └──────────────────────────┘
txt └──────────────────────────┘
par └──────────────────────────┘
pid └────────────────────┘
st ───────────────────────────────┘└─
328 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
329 { rw ← coinduced_le_iff_le_induced, exact lattice.le_sup_left },
id └─────────────────────────┘ └─────────────────┘
src └───┘└─────────────────────────┘ └────┘└─────────────────┘┴
typ └───┘└─────────────────────────┘ └────┘└─────────────────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └─┘ ┴ ┴
st ─────┘└──────────────────────────────┘└──────────────────────────┘└┘└
330 { intros u hu, existsi (sum.inl '' u),
id └─────┘ └┘ ┴
src └─────────┘ └──────┘ └─────┘┴└┘┴ ┴
typ └─────────┘ └──────┘ └─────┘┴└┘┴┴┴
doc └─────────┘ └──────┘ ┴ ┴ ┴
txt └─────────┘ └──────┘ ┴ ┴ ┴
par └─────────┘ └──────┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴
st ────────────────┘└──────────────────────┘└─
331 change
src └──────
typ └──────
doc └──────
txt └──────
par └──────
pid └
st ─────────────
332 (is_open (sum.inl ⁻¹' (@sum.inl α β '' u)) ∧
id └─┘
src ───────┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
typ ───────┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
doc ───────┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────
333 is_open (sum.inr ⁻¹' (@sum.inl α β '' u))) ∧
id └─────┘ └─────┘ ┴ ┴
src ────────┘└─────┘┴ └─────┘┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
typ ────────┘└─────┘┴ └─────┘┴ ┴ ┴┴┴┴┴ ┴ └──┘ └
doc ────────┘└─────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
txt ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
par ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
pid ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────────────────────────────
334 sum.inl ⁻¹' (sum.inl '' u) = u,
id └─────┘ ┴ ┴
src ───────┘ ┴ ┴ └─────┘┴ ┴ └┘┴┴
typ ───────┘ ┴ ┴ └─────┘┴ ┴ └┘┴┴┴
doc ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────┘└─
335 have : sum.inl ⁻¹' (@sum.inl α β '' u) = u :=
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘┴ ┴ ┴ ┴ └┘ ┴ └───
typ └─────┘ ┴ ┴ └─────┘┴┴┴┴┴ ┴ └┘ ┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
st ────────────────────────────────────────────────────
336 preimage_image_eq u (λ _ _, sum.inl.inj_iff.mp), rw this,
id └───────────────┘ ┴ └────────────────┘ └──┘
src ───────┘└───────────────┘┴ ┴ └────┘└────────────────┘┴ └─┘
typ ───────┘└───────────────┘┴┴┴ └────┘└────────────────┘┴ └─┘└──┘
doc ───────┘ ┴ ┴ └────┘ ┴ └─┘
txt ───────┘ ┴ ┴ └────┘ ┴ └─┘
par ───────┘ ┴ ┴ └────┘ ┴ └─┘
pid ───────┘ ┴ ┴ └────┘ ┴ ┴
st ──────────────────────────────────────────────────────┘└───────┘└─
337 have : sum.inr ⁻¹' (@sum.inl α β '' u) = ∅ :=
id └─────┘ └─────┘ ┴ ┴ ┴ ┴
src └─────┘└─────┘┴ ┴ └─────┘┴ ┴ ┴ ┴ └┘ ┴┴└───
typ └─────┘└─────┘┴ ┴ └─────┘┴┴┴┴┴ ┴┴└┘ ┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
st ────────────────────────────────────────────────────
338 eq_empty_iff_forall_not_mem.mpr (assume a ⟨b, _, h⟩, sum.inl_ne_inr h), rw this,
id └─────────────────────────────┘ ┴ └────────────┘ └──┘
src ───────┘└─────────────────────────────┘┴ └──┘ └───┘ └─┘└────────────┘┴ ┴ └─┘
typ ───────┘└─────────────────────────────┘┴ └──┘ └───┘┴└─┘└────────────┘┴ ┴ └─┘└──┘
doc ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
txt ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
par ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
pid ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└───────┘└─
339 exact ⟨⟨hu, is_open_empty⟩, rfl⟩ }
id └┘ └───────────┘ └─┘
src └────┘ └┘└───────────┘└─┘└─┘└┘
typ └────┘ └┘└┘└───────────┘└─┘└─┘└┘
doc └────┘ └┘ └─┘ └┘
txt └────┘ └┘ └─┘ └┘
par └────┘ └┘ └─┘ └┘
pid ┴ └┘ └─┘ ┴┴
st ──────────────────────────────────────┘└─
340 end,
st ────┘
341 inj := λ _ _, sum.inl.inj_iff.mp }
id ┴ ┴ └─────────────┘└─┘
src └─────────────┘└─┘
typ ┴ ┴ └─────────────┘└─┘
342
343 lemma embedding_inr : embedding (@sum.inr α β) :=
id └───────┘ └─────┘ ┴ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴ ┴
doc └───────┘
344 { induced := begin
st └─────
345 unfold sum.topological_space,
src └──────────────────────────┘
typ └──────────────────────────┘
doc └──────────────────────────┘
txt └──────────────────────────┘
par └──────────────────────────┘
pid └────────────────────┘
st ───────────────────────────────┘└─
346 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
347 { rw ← coinduced_le_iff_le_induced, exact lattice.le_sup_right },
id └─────────────────────────┘ └──────────────────┘
src └───┘└─────────────────────────┘ └────┘└──────────────────┘┴
typ └───┘└─────────────────────────┘ └────┘└──────────────────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └─┘ ┴ ┴
st ─────┘└──────────────────────────────┘└───────────────────────────┘└┘└
348 { intros u hu, existsi (sum.inr '' u),
id └─────┘ └┘ ┴
src └─────────┘ └──────┘ └─────┘┴└┘┴ ┴
typ └─────────┘ └──────┘ └─────┘┴└┘┴┴┴
doc └─────────┘ └──────┘ ┴ ┴ ┴
txt └─────────┘ └──────┘ ┴ ┴ ┴
par └─────────┘ └──────┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴
st ────────────────┘└──────────────────────┘└─
349 change
src └──────
typ └──────
doc └──────
txt └──────
par └──────
pid └
st ─────────────
350 (is_open (sum.inl ⁻¹' (@sum.inr α β '' u)) ∧
id └─────┘ └─┘
src ───────┘ ┴ └─────┘┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
typ ───────┘ ┴ └─────┘┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
doc ───────┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ └─┘ └
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────
351 is_open (sum.inr ⁻¹' (@sum.inr α β '' u))) ∧
id └─────┘ ┴ ┴
src ────────┘└─────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
typ ────────┘└─────┘┴ ┴ ┴ ┴┴┴┴┴ ┴ └──┘ └
doc ────────┘└─────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
txt ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
par ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
pid ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────────────────────────────
352 sum.inr ⁻¹' (sum.inr '' u) = u,
id └─────┘ ┴ ┴
src ───────┘ ┴ ┴ └─────┘┴ ┴ └┘┴┴
typ ───────┘ ┴ ┴ └─────┘┴ ┴ └┘┴┴┴
doc ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────┘└─
353 have : sum.inl ⁻¹' (@sum.inr α β '' u) = ∅ :=
id └─────┘ └─────┘ ┴ ┴ ┴ ┴
src └─────┘└─────┘┴ ┴ └─────┘┴ ┴ ┴ ┴ └┘ ┴┴└───
typ └─────┘└─────┘┴ ┴ └─────┘┴┴┴┴┴ ┴┴└┘ ┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
st ────────────────────────────────────────────────────
354 eq_empty_iff_forall_not_mem.mpr (assume b ⟨a, _, h⟩, sum.inr_ne_inl h), rw this,
id └─────────────────────────────┘ ┴ └────────────┘ └──┘
src ───────┘└─────────────────────────────┘┴ └──┘ └───┘ └─┘└────────────┘┴ ┴ └─┘
typ ───────┘└─────────────────────────────┘┴ └──┘ └───┘┴└─┘└────────────┘┴ ┴ └─┘└──┘
doc ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
txt ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
par ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ └─┘
pid ───────┘ ┴ └──┘ └───┘ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└───────┘└─
355 have : sum.inr ⁻¹' (@sum.inr α β '' u) = u :=
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘┴ ┴ ┴ ┴ └┘ ┴ └───
typ └─────┘ ┴ ┴ └─────┘┴┴┴┴┴ ┴ └┘ ┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───
st ────────────────────────────────────────────────────
356 preimage_image_eq u (λ _ _, sum.inr.inj_iff.mp), rw this,
id └───────────────┘ ┴ └────────────────┘ └──┘
src ───────┘└───────────────┘┴ ┴ └────┘└────────────────┘┴ └─┘
typ ───────┘└───────────────┘┴┴┴ └────┘└────────────────┘┴ └─┘└──┘
doc ───────┘ ┴ ┴ └────┘ ┴ └─┘
txt ───────┘ ┴ ┴ └────┘ ┴ └─┘
par ───────┘ ┴ ┴ └────┘ ┴ └─┘
pid ───────┘ ┴ ┴ └────┘ ┴ ┴
st ──────────────────────────────────────────────────────┘└───────┘└─
357 exact ⟨⟨is_open_empty, hu⟩, rfl⟩ }
id └───────────┘ └┘ └─┘
src └────┘ └───────────┘└┘ └─┘└─┘└┘
typ └────┘ └───────────┘└┘└┘└─┘└─┘└┘
doc └────┘ └┘ └─┘ └┘
txt └────┘ └┘ └─┘ └┘
par └────┘ └┘ └─┘ └┘
pid ┴ └┘ └─┘ ┴┴
st ──────────────────────────────────────┘└─
358 end,
st ────┘
359 inj := λ _ _, sum.inr.inj_iff.mp }
id ┴ ┴ └─────────────┘└─┘
src └─────────────┘└─┘
typ ┴ ┴ └─────────────┘└─┘
360
361 end sum
362
363 section subtype
364 variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
id └───────────────┘ └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘ └───────────────┘
365
366 lemma embedding_subtype_val : embedding (@subtype.val α p) :=
id └───────┘ └─────────┘ ┴ ┴
src └───────┘ └─────────┘
typ └───────┘ └─────────┘ ┴ ┴
doc └───────┘
367 ⟨⟨rfl⟩, subtype.val_injective⟩
id └─┘ └───────────────────┘
src └─┘ └───────────────────┘
typ └─┘ └───────────────────┘
368
369 lemma continuous_subtype_val : continuous (@subtype.val α p) :=
id └────────┘ └─────────┘ ┴ ┴
src └────────┘ └─────────┘
typ └────────┘ └─────────┘ ┴ ┴
doc └────────┘
370 continuous_induced_dom
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
371
372 lemma is_open.open_embedding_subtype_val {s : set α} (hs : is_open s) :
id └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴
doc └─────┘
373 open_embedding (subtype.val : s → α) :=
id └────────────┘ └─────────┘ ┴ ┴
src └────────────┘ └─────────┘
typ └────────────┘ └─────────┘ ┴ ┴
doc └────────────┘
374 { induced := rfl,
id └─┘
src └─┘
typ └─┘
375 inj := subtype.val_injective,
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
376 open_range := (subtype.val_range : range subtype.val = s).symm ▸ hs }
id └───────────────┘ └───┘ └─────────┘ ┴ ┴ └──┘ ┴ └┘
src └───────────────┘ └───┘ └─────────┘ ┴ └──┘ ┴
typ └───────────────┘ └───┘ └─────────┘ ┴ ┴ └──┘ ┴ └┘
doc └───┘
377
378 lemma is_open.is_open_map_subtype_val {s : set α} (hs : is_open s) :
id └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴
doc └─────┘
379 is_open_map (subtype.val : s → α) :=
id └─────────┘ └─────────┘ ┴ ┴
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ ┴ ┴
doc └─────────┘
380 hs.open_embedding_subtype_val.is_open_map
id └┘└─────────────────────────┘└──────────┘
src └─────────────────────────┘└──────────┘
typ └┘└─────────────────────────┘└──────────┘
381
382 lemma is_open_map.restrict {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
id ┴ ┴ └─────────┘ ┴ └─┘ ┴ └─────┘ ┴
src └─────────┘ └─┘ └─────┘
typ ┴ ┴ └─────────┘ ┴ └─┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
383 is_open_map (function.restrict f s) :=
id └─────────┘ └───────────────┘ ┴ ┴
src └─────────┘ └───────────────┘
typ └─────────┘ └───────────────┘ ┴ ┴
doc └─────────┘
384 hf.comp hs.is_open_map_subtype_val
id └┘└───┘ └┘└──────────────────────┘
src └───┘ └──────────────────────┘
typ └┘└───┘ └┘└──────────────────────┘
385
386 lemma is_closed.closed_embedding_subtype_val {s : set α} (hs : is_closed s) :
id └─┘ ┴ └───────┘ ┴
src └─┘ └───────┘
typ └─┘ ┴ └───────┘ ┴
doc └───────┘
387 closed_embedding (subtype.val : {x // x ∈ s} → α) :=
id └──────────────┘ └─────────┘ ┴┴ ┴ ┴ ┴ ┴
src └──────────────┘ └─────────┘ ┴ ┴
typ └──────────────┘ └─────────┘ ┴┴ ┴ ┴ ┴ ┴
doc └──────────────┘
388 { induced := rfl,
id └─┘
src └─┘
typ └─┘
389 inj := subtype.val_injective,
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
390 closed_range := (subtype.val_range : range subtype.val = s).symm ▸ hs }
id └───────────────┘ └───┘ └─────────┘ ┴ ┴ └──┘ ┴ └┘
src └───────────────┘ └───┘ └─────────┘ ┴ └──┘ ┴
typ └───────────────┘ └───┘ └─────────┘ ┴ ┴ └──┘ ┴ └┘
doc └───┘
391
392 lemma continuous_subtype_mk {f : β → α}
id ┴ ┴
typ ┴ ┴
393 (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴
src └────────┘ └────────┘ └─────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴
doc └────────┘ └────────┘
394 continuous_induced_rng h
id └────────────────────┘ ┴
src └────────────────────┘
typ └────────────────────┘ ┴
395
396 lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) :=
id └─┘ ┴ ┴ ┴ ┴ └────────┘ └───────┘ ┴
src └─┘ ┴ └────────┘ └───────┘
typ └─┘ ┴ ┴ ┴ ┴ └────────┘ └───────┘ ┴
doc └────────┘ └───────┘
397 continuous_subtype_mk _ continuous_subtype_val
id └───────────────────┘ └────────────────────┘
src └───────────────────┘ └────────────────────┘
typ └───────────────────┘ └────────────────────┘
398
399 lemma continuous_at_subtype_val {p : α → Prop} {a : subtype p} :
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
400 continuous_at subtype.val a :=
id └───────────┘ └─────────┘ ┴
src └───────────┘ └─────────┘
typ └───────────┘ └─────────┘ ┴
doc └───────────┘
401 continuous_iff_continuous_at.mp continuous_subtype_val _
id └──────────────────────────┘└─┘ └────────────────────┘
src └──────────────────────────┘└─┘ └────────────────────┘
typ └──────────────────────────┘└─┘ └────────────────────┘
402
403 lemma map_nhds_subtype_val_eq {a : α} (ha : p a) (h : {a | p a} ∈ 𝓝 a) :
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴
404 map (@subtype.val α p) (𝓝 ⟨a, ha⟩) = 𝓝 a :=
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ └─────────┘ ┴ ┴ ┴
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘ ┴ ┴
405 map_nhds_induced_eq (by simp [subtype.val_image, h])
id └─────────────────┘ └───────────────┘ ┴
src └─────────────────┘ └────┘└───────────────┘└┘ ┴
typ └─────────────────┘ └────┘└───────────────┘└┘┴┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └──────────────────────────┘
406
407 lemma nhds_subtype_eq_comap {a : α} {h : p a} :
id ┴ ┴ ┴
typ ┴ ┴ ┴
408 𝓝 (⟨a, h⟩ : subtype p) = comap subtype.val (𝓝 a) :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ └───┘ └─────────┘ ┴ ┴
src ┴ └─────┘ ┴ └───┘ └─────────┘ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ └───┘ └─────────┘ ┴ ┴
doc ┴ └───┘ ┴
409 nhds_induced _ _
id └──────────┘
src └──────────┘
typ └──────────┘
410
411 lemma tendsto_subtype_rng {β : Type*} {p : α → Prop} {b : filter β} {f : β → subtype p} :
id ┴ └────┘ ┴ ┴ └─────┘ ┴
src └────┘ └─────┘
typ ┴ └────┘ ┴ ┴ └─────┘ ┴
412 ∀{a:subtype p}, tendsto f b (𝓝 a) ↔ tendsto (λx, subtype.val (f x)) b (𝓝 a.val)
id ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└──┘
src └─────┘ └─────┘ ┴ ┴ └─────┘ └─────────┘ ┴ └──┘
typ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└──┘
doc └─────┘ ┴ └─────┘ ┴
413 | ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff]
id └───────────────────┘ └───────────────┘
src └──┘└───────────────────┘└┘└───────────────┘└─
typ └──┘└───────────────────┘└┘└───────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────┘└─────────────────┘┴└
414
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
415 lemma continuous_subtype_nhds_cover {ι : Sort*} {f : α → β} {c : ι → α → Prop}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
416 (c_cover : ∀x:α, ∃i, {x | c i x} ∈ 𝓝 x)
id ┴ ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
417 (f_cont : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
id ┴ └────────┘ └─────┘ ┴ ┴ ┴ ┴└──┘
src └────────┘ └─────┘ └──┘
typ ┴ └────────┘ └─────┘ ┴ ┴ ┴ ┴└──┘
doc └────────┘
418 continuous f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
419 continuous_iff_continuous_at.mpr $ assume x,
id └──────────────────────────┘└──┘ ┴
src └──────────────────────────┘└──┘
typ └──────────────────────────┘└──┘ ┴
420 let ⟨i, (c_sets : {x | c i x} ∈ 𝓝 x)⟩ := c_cover x in
id └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc ┴
421 let x' : subtype (c i) := ⟨x, mem_of_nhds c_sets⟩ in
id └─────┘ ┴ ┴ └─────────┘
src └─────┘ └─────────┘
typ └─────┘ ┴ ┴ └─────────┘
422 calc map f (𝓝 x) = map f (map subtype.val (𝓝 x')) :
id └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─────────┘ ┴ └┘
src └─┘ ┴ └─┘ └─┘ └─────────┘ ┴
typ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └─────────┘ ┴ └┘
doc └─┘ ┴ └─┘ └─┘ ┴
423 congr_arg (map f) (map_nhds_subtype_val_eq _ $ c_sets).symm
id └───────┘ └─┘ ┴ └─────────────────────┘ └──┘
src └───────┘ └─┘ └─────────────────────┘ └──┘
typ └───────┘ └─┘ ┴ └─────────────────────┘ └──┘
doc └─┘
424 ... = map (λx:subtype (c i), f x.val) (𝓝 x') : rfl
id └─┘ └─────┘ ┴ ┴ ┴└──┘ ┴ └┘ └─┘
src └─┘ └─────┘ └──┘ ┴ └─┘
typ └─┘ └─────┘ ┴ ┴ ┴└──┘ ┴ └┘ └─┘
doc └─┘ ┴
425 ... ≤ 𝓝 (f x) : continuous_iff_continuous_at.mp (f_cont i) x'
id ┴ ┴ ┴ └──────────────────────────┘└─┘ └────┘ └┘
src ┴ └──────────────────────────┘└─┘
typ ┴ ┴ ┴ └──────────────────────────┘└─┘ └────┘ └┘
doc ┴
426
427 lemma continuous_subtype_is_closed_cover {ι : Sort*} {f : α → β} (c : ι → α → Prop)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
428 (h_lf : locally_finite (λi, {x | c i x}))
id └────────────┘ ┴ ┴┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴┴ ┴ ┴ ┴
doc └────────────┘
429 (h_is_closed : ∀i, is_closed {x | c i x})
id ┴ └───────┘ ┴┴ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ └───────┘ ┴┴ ┴ ┴ ┴
doc └───────┘
430 (h_cover : ∀x, ∃i, c i x)
id ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴
431 (f_cont : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
id ┴ └────────┘ └─────┘ ┴ ┴ ┴ ┴└──┘
src └────────┘ └─────┘ └──┘
typ ┴ └────────┘ └─────┘ ┴ ┴ ┴ ┴└──┘
doc └────────┘
432 continuous f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
433 continuous_iff_is_closed.mpr $
id └──────────────────────┘└──┘
src └──────────────────────┘└──┘
typ └──────────────────────┘└──┘
434 assume s hs,
id ┴ └┘
typ ┴ └┘
435 have ∀i, is_closed (@subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id ┴ └───────┘ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
src └───────┘ └─────────┘ ┴ └┘ ┴ └─────────┘ └─┘
typ ┴ └───────┘ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
doc └───────┘ └─┘
436 from assume i,
id ┴
typ ┴
437 embedding_is_closed embedding_subtype_val
id └─────────────────┘ └───────────────────┘
src └─────────────────┘ └───────────────────┘
typ └─────────────────┘ └───────────────────┘
438 (by simp [subtype.val_range]; exact h_is_closed i)
id └───────────────┘ └─────────┘ ┴
src └────┘└───────────────┘┴ └────┘ ┴
typ └────┘└───────────────┘┴ └────┘└─────────┘┴┴
doc └────┘ ┴ └────┘ ┴
txt └────┘ ┴ └────┘ ┴
par └────┘ ┴ └────┘ ┴
pid ┴┴ ┴ ┴ ┴
st └────────────────────────────────────────────┘
439 (continuous_iff_is_closed.mp (f_cont i) _ hs),
id └──────────────────────┘└─┘ └────┘ ┴ └┘
src └──────────────────────┘└─┘
typ └──────────────────────┘└─┘ └────┘ ┴ └┘
440 have is_closed (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id └───────┘ ┴┴┴ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
src └───────┘ ┴ ┴ └─────────┘ ┴ └┘ ┴ └─────────┘ └─┘
typ └───────┘ ┴┴┴ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
doc └───────┘ ┴ ┴ └─┘
441 from is_closed_Union_of_locally_finite
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
442 (locally_finite_subset h_lf $ assume i x ⟨⟨x', hx'⟩, _, heq⟩, heq ▸ hx')
id └───────────────────┘ └──┘ ┴ ┴ ┴ └─┘ └─┘ ┴
src └───────────────────┘ └─┘ ┴
typ └───────────────────┘ └──┘ ┴ ┴ ┴ └─┘ └─┘ ┴
443 this,
id └──┘
typ └──┘
444 have f ⁻¹' s = (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
id ┴ └─┘ ┴ ┴ ┴┴┴ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
src └─┘ ┴ ┴ ┴ └─────────┘ ┴ └┘ ┴ └─────────┘ └─┘
typ ┴ └─┘ ┴ ┴ ┴┴┴ └─────────┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘ └─┘ ┴
doc └─┘ ┴ ┴ └─┘
445 begin
st └─────
446 apply set.ext,
id └─────┘
src └────┘└─────┘
typ └────┘└─────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
447 have : ∀ (x : α), f x ∈ s ↔ ∃ (i : ι), c i x ∧ f x ∈ s :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴└────┘ ┴┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └───
typ └─────┘ └────┘┴┴ ┴ ┴ ┴┴┴ ┴ ┴┴└────┘┴┴┴┴┴┴ ┴ ┴┴┴┴┴ ┴ ┴┴└───
doc └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
txt └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────
448 λ x, ⟨λ hx, let ⟨i, hi⟩ := h_cover x in ⟨i, hi, hx⟩,
id ┴ └┘ └─────┘
src ─────┘ └──┘ └───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └┘ └──
typ ─────┘ └──┘ └───┘ ┴ ┴└┘└┘└───┘└─────┘┴ └──┘ └┘ └┘ └──
doc ─────┘ └──┘ └───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └┘ └──
txt ─────┘ └──┘ └───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └┘ └──
par ─────┘ └──┘ └───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └┘ └──
pid ─────┘ └──┘ └───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └┘ └──
st ───────────────────────────────────────────────────────────
449 λ ⟨i, hi, hx⟩, hx⟩,
id └┘
src ───────────┘ └┘ └┘ └┘ └─┘ ┴
typ ───────────┘ └┘ └┘ └┘└┘└─┘ ┴
doc ───────────┘ └┘ └┘ └┘ └─┘ ┴
txt ───────────┘ └┘ └┘ └┘ └─┘ ┴
par ───────────┘ └┘ └┘ └┘ └─┘ ┴
pid ───────────┘ └┘ └┘ └┘ └─┘ ┴
st ─────────────────────────────┘└─
450 simp [and.comm, and.left_comm], simpa [(∘)],
id └──────┘ └───────────┘ ┴
src └────┘└──────┘└┘└───────────┘┴ └─────┘┴└─┘
typ └────┘└──────┘└┘└───────────┘┴ └─────┘┴└─┘
doc └────┘ └┘ ┴ └─────┘ └─┘
txt └────┘ └┘ ┴ └─────┘ └─┘
par └────┘ └┘ ┴ └─────┘ └─┘
pid ┴┴ └┘ ┴ ┴┴ └─┘
st ─────────────────────────────────┘└───────────┘└─
451 end,
st ────┘
452 by rwa [this]
id └──┘
src └───┘ └─
typ └───┘└──┘└─
doc └───┘ └─
txt └───┘ └─
par └───┘ └─
pid └┘ ┴└
st └────────┘┴└
453
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
454 lemma closure_subtype {x : {a // p a}} {s : set {a // p a}}:
id ┴┴ ┴ ┴ └─┘ ┴┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴┴ ┴ ┴ └─┘ ┴┴ ┴ ┴
455 x ∈ closure s ↔ x.val ∈ closure (subtype.val '' s) :=
id ┴ ┴ └─────┘ ┴ ┴ ┴└──┘ ┴ └─────┘ └─────────┘ └┘ ┴
src ┴ └─────┘ ┴ └──┘ ┴ └─────┘ └─────────┘ └┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴└──┘ ┴ └─────┘ └─────────┘ └┘ ┴
doc └─────┘ └─────┘
456 closure_induced $ assume x y, subtype.eq
id └─────────────┘ ┴ ┴ └────────┘
src └─────────────┘ └────────┘
typ └─────────────┘ ┴ ┴ └────────┘
457
458 end subtype
459
460 section quotient
461 variables [topological_space α] [topological_space β] [topological_space γ]
id └───────────────┘ └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘ └───────────────┘
462 variables {r : α → α → Prop} {s : setoid α}
id └────┘
src └────┘
typ └────┘
463
464 lemma quotient_map_quot_mk : quotient_map (@quot.mk α r) :=
id └──────────┘ └─────┘ ┴ ┴
src └──────────┘
typ └──────────┘ └─────┘ ┴ ┴
doc └──────────┘
465 ⟨quot.exists_rep, rfl⟩
id └─────────────┘ └─┘
src └─────────────┘ └─┘
typ └─────────────┘ └─┘
466
467 lemma continuous_quot_mk : continuous (@quot.mk α r) :=
id └────────┘ └─────┘ ┴ ┴
src └────────┘
typ └────────┘ └─────┘ ┴ ┴
doc └────────┘
468 continuous_coinduced_rng
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
469
470 lemma continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
471 (h : continuous f) : continuous (quot.lift f hr : quot r → β) :=
id └────────┘ ┴ └────────┘ └───────┘ ┴ └┘ └──┘ ┴ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ └───────┘ ┴ └┘ └──┘ ┴ ┴
doc └────────┘ └────────┘
472 continuous_coinduced_dom h
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
473
474 lemma quotient_map_quotient_mk : quotient_map (@quotient.mk α s) :=
id └──────────┘ └─────────┘ ┴ ┴
src └──────────┘ └─────────┘
typ └──────────┘ └─────────┘ ┴ ┴
doc └──────────┘
475 quotient_map_quot_mk
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
476
477 lemma continuous_quotient_mk : continuous (@quotient.mk α s) :=
id └────────┘ └─────────┘ ┴ ┴
src └────────┘ └─────────┘
typ └────────┘ └─────────┘ ┴ ┴
doc └────────┘
478 continuous_coinduced_rng
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
479
480 lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
481 (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
id └────────┘ ┴ └────────┘ └───────────┘ ┴ └┘ └──────┘ ┴ ┴
src └────────┘ └────────┘ └───────────┘ └──────┘
typ └────────┘ ┴ └────────┘ └───────────┘ ┴ └┘ └──────┘ ┴ ┴
doc └────────┘ └────────┘
482 continuous_coinduced_dom h
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
483
484 end quotient
485
486 section pi
487 variables {ι : Type*} {π : ι → Type*}
488 open topological_space
489
490 lemma continuous_pi [topological_space α] [∀i, topological_space (π i)] {f : α → Πi:ι, π i}
id └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └───────────────┘
491 (h : ∀i, continuous (λa, f a i)) : continuous f :=
id ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
492 continuous_infi_rng $ assume i, continuous_induced_rng $ h i
id └─────────────────┘ ┴ └────────────────────┘ ┴ ┴
src └─────────────────┘ └────────────────────┘
typ └─────────────────┘ ┴ └────────────────────┘ ┴ ┴
493
494 lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
id ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ ┴ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘
495 continuous (λp:Πi, π i, p i) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘
496 continuous_infi_dom continuous_induced_dom
id └─────────────────┘ └────────────────────┘
src └─────────────────┘ └────────────────────┘
typ └─────────────────┘ └────────────────────┘
497
498 /-- Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is
499 continuous. -/
500 lemma continuous_update [decidable_eq ι] [∀i, topological_space (π i)] {i : ι} {f : Πi:ι, π i} :
id └──────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └───────────────┘
typ └──────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘
501 continuous (λ x : π i, function.update f i x) :=
id └────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └────────┘ └─────────────┘
typ └────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └────────┘ └─────────────┘
502 begin
st └─────
503 refine continuous_pi (λj, _),
id └───────────┘
src └─────┘└───────────┘┴ └───┘
typ └─────┘└───────────┘┴ └───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────────┘└─
504 by_cases h : j = i,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────┘└─
505 { rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└──┘└─
506 simpa using continuous_id },
id └───────────┘
src └──────────┘└───────────┘┴
typ └──────────┘└───────────┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ─────────────────────────────┘└┘└
507 { simpa [h] using continuous_const }
id ┴ └──────────────┘
src └─────┘ └──────┘└──────────────┘┴
typ └─────┘┴└──────┘└──────────────┘┴
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st ────────────────────────────────────┘└─
508 end
st ──┘
509
510 lemma nhds_pi [t : ∀i, topological_space (π i)] {a : Πi, π i} :
id ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────┘
typ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘
511 𝓝 a = (⨅i, comap (λx, x i) (𝓝 (a i))) :=
id ┴ ┴ ┴ ┴┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ └───┘ ┴
512 calc 𝓝 a = (⨅i, @nhds _ (@topological_space.induced _ _ (λx:Πi, π i, x i) (t i)) a) : nhds_infi
id ┴ ┴ ┴┴┴ └──┘ └───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src ┴ ┴ ┴ └──┘ └───────────────────────┘ └───────┘
typ ┴ ┴ ┴┴┴ └──┘ └───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
doc ┴ ┴ ┴ └──┘ └───────────────────────┘
513 ... = (⨅i, comap (λx, x i) (𝓝 (a i))) : by simp [nhds_induced]
id ┴┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
src ┴ ┴ └───┘ ┴ └────┘└──────────┘└─
typ ┴┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────────┘└─
doc ┴ ┴ └───┘ ┴ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────
514
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
515 lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)}
id ┴ └───────────────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └───────────────┘ └─┘ └─┘
typ ┴ └───────────────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └───────────────┘
516 (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) :=
id └────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ └┘ ┴ ┴
src └────┘ ┴ └─────┘ └─────┘ └┘
typ └────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ └┘ ┴ ┴
doc └────┘ └─────┘ └─────┘ └┘
517 by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, continuous_apply a _ $ hs a ha)
id └────┘ └────────────┘ └┘ └──────────────┘ └┘
src └──┘└────┘┴ └────┘ └────────────┘┴ ┴ ┴ └─────┘└──────────────┘┴ └─┘ ┴ ┴ ┴ └─
typ └──┘└────┘┴ └────┘ └────────────┘┴└┘┴ ┴ └─────┘└──────────────┘┴ └─┘ ┴└┘┴ ┴ └─
doc └──┘ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─
txt └──┘ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─
par └──┘ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴└
st └─────────┘┴└─────────────────────────────────────────────────────────────────────────
518
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
519 lemma pi_eq_generate_from [∀a, topological_space (π a)] :
id ┴ └───────────────┘ ┴ ┴
src └───────────────┘
typ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘
520 Pi.topological_space =
id └──────────────────┘ ┴
src └──────────────────┘ ┴
typ └──────────────────┘ ┴
521 generate_from {g | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, is_open (s a)) ∧ g = pi ↑i s} :=
id └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
src └───────────┘ ┴ ┴ └─┘ └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴
typ └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
doc └───────────┘ └────┘ └─────┘ └┘
522 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
523 (le_generate_from $ assume g ⟨s, i, hi, eq⟩, eq.symm ▸ is_open_set_pi (finset.finite_to_set _) hi)
id └──────────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └────────────┘ └──────────────────┘
src └──────────────┘ └┘ └───┘ ┴ └────────────┘ └──────────────────┘
typ └──────────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └────────────┘ └──────────────────┘
524 (le_infi $ assume a s ⟨t, ht, s_eq⟩, generate_open.basic _ $
id └─────┘ ┴ ┴ ┴┴ └─────────────────┘
src └─────┘ └─────────────────┘
typ └─────┘ ┴ ┴ ┴┴ └─────────────────┘
525 ⟨function.update (λa, univ) a t, {a}, by simpa using ht, by ext f; simp [s_eq.symm, pi]⟩)
id └─────────────┘ ┴ └──┘ ┴ ┴┴ └┘ └┘
src └─────────────┘ └──┘ ┴ └──────────┘ └───┘ └────┘ └┘└┘┴
typ └─────────────┘ ┴ └──┘ ┴ ┴┴ └──────────┘└┘ └───┘ └────┘└───────┘└┘└┘┴
doc └─────────────┘ └──────────┘ └───┘ └────┘ └┘└┘┴
txt └──────────┘ └───┘ └────┘ └┘ ┴
par └──────────┘ └───┘ └────┘ └┘ ┴
pid ┴└────┘ └┘ ┴┴ └┘ ┴
st └─────────────┘ └──────────────────────────┘
526
527 lemma pi_generate_from_eq {g : Πa, set (set (π a))} :
id ┴ └─┘ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴
528 @Pi.topological_space ι π (λa, generate_from (g a)) =
id └──────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └──────────────────┘ └───────────┘ ┴
typ └──────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
529 generate_from {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s} :=
id └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
src └───────────┘ ┴ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴
typ └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
doc └───────────┘ └────┘ └┘
530 let G := {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s} in
id ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
src ┴ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴
doc └────┘ └┘
531 begin
st └─────
532 rw [pi_eq_generate_from],
id └─────────────────┘
src └──┘└─────────────────┘┴
typ └──┘└─────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────────┘└──
533 refine le_antisymm (generate_from_mono _) (le_generate_from _),
id └─────────┘ └────────────────┘ └──────────────┘
src └─────┘└─────────┘┴ └────────────────┘└──┘ └──────────────┘└─┘
typ └─────┘└─────────┘┴ └────────────────┘└──┘ └──────────────┘└─┘
doc └─────┘ ┴ └──┘ └─┘
txt └─────┘ ┴ └──┘ └─┘
par └─────┘ ┴ └──┘ └─┘
pid ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────────────────────────┘└─
534 exact assume s ⟨t, i, ht, eq⟩, ⟨t, i, assume a ha, generate_open.basic _ (ht a ha), eq⟩,
id ┴ ┴ └┘ └┘ └─────────────────┘
src └────┘ └──┘ └┘ └┘ └┘└┘└─┘ └┘ └┘ └─────┘└─────────────────┘└─┘ ┴ ┴ └─┘ ┴
typ └────┘ └──┘┴└┘┴└┘└┘└┘└┘└─┘ └┘ └┘ └─────┘└─────────────────┘└─┘ ┴ ┴ └─┘ ┴
doc └────┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴
txt └────┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴
par └────┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴
pid ┴ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
535 { rintros s ⟨t, i, hi, rfl⟩,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └────────────────┘
st ────────────────────────────┘└─
536 rw [pi_def],
id └────┘
src └──┘└────┘┴
typ └──┘└────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────┘└──
537 apply is_open_bInter (finset.finite_to_set _),
id └────────────┘ └──────────────────┘
src └────┘└────────────┘┴ └──────────────────┘└─┘
typ └────┘└────────────┘┴ └──────────────────┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ────────────────────────────────────────────────┘└─
538 assume a ha, show ((generate_from G).coinduced (λf:Πa, π a, f a)).is_open (t a),
id └───────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └───┘ └───────────┘┴ └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─────────┘ ┴ ┴
typ └─────────┘ └───┘ └───────────┘┴┴└──────────┘ └┘ ┴ ┴┴┴ └┘ ┴ └─────────┘ ┴┴┴┴
doc └─────────┘ └───┘ └───────────┘┴ └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─────────┘ ┴ ┴
txt └─────────┘ └───┘ ┴ └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─────────┘ ┴ ┴
par └─────────┘ └───┘ ┴ └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─────────┘ ┴ ┴
pid └─────────┘ └───┘ ┴ └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─────────┘ ┴ ┴
st ──────────────┘└──────────────────────────────────────────────────────────────────┘└─
539 refine le_generate_from _ _ (hi a ha),
id └──────────────┘ └┘ ┴ └┘
src └─────┘└──────────────┘└───┘ ┴ ┴ ┴
typ └─────┘└──────────────┘└───┘ └┘┴┴┴└┘┴
doc └─────┘ └───┘ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴
pid ┴ └───┘ ┴ ┴ ┴
st ────────────────────────────────────────┘└─
540 exact assume s hs, generate_open.basic _ ⟨function.update (λa, univ) a s, {a}, by simp [hs]⟩ }
id └─────────────────┘ └─────────────┘ └──┘ ┴ └┘
src └────┘ └─────┘└─────────────────┘└─┘ └─────────────┘┴ └─┘└──┘└┘ ┴ └┘┴└──┘ ┴└────┘ ┴└┘
typ └────┘ └─────┘└─────────────────┘└─┘ └─────────────┘┴ └─┘└──┘└┘ ┴ └┘┴└──┘ ┴└────┘└┘┴└┘
doc └────┘ └─────┘ └─┘ └─────────────┘┴ └─┘ └┘ ┴ └┘ └──┘ ┴└────┘ ┴└┘
txt └────┘ └─────┘ └─┘ ┴ └─┘ └┘ ┴ └┘ └──┘ ┴└────┘ ┴└┘
par └────┘ └─────┘ └─┘ ┴ └─┘ └┘ ┴ └┘ └──┘ ┴└────┘ ┴└┘
pid ┴ └─────┘ └─┘ ┴ └─┘ └┘ ┴ └┘ └──┘ └─────┘ └┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘└────────┘└┘└─
541 end
st ──┘
542
543 lemma pi_generate_from_eq_fintype {g : Πa, set (set (π a))} [fintype ι] (hg : ∀a, ⋃₀ g a = univ) :
id ┴ └─┘ └─┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘
src └─┘ └─┘ └─────┘ └┘ ┴ └──┘
typ ┴ └─┘ └─┘ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘
doc └─────┘
544 @Pi.topological_space ι π (λa, generate_from (g a)) =
id └──────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └──────────────────┘ └───────────┘ ┴
typ └──────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
545 generate_from {t | ∃(s:Πa, set (π a)), (∀a, s a ∈ g a) ∧ t = pi univ s} :=
id └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ ┴
src └───────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘
typ └───────────┘ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ ┴
doc └───────────┘ └┘
546 let G := {t | ∃(s:Πa, set (π a)), (∀a, s a ∈ g a) ∧ t = pi univ s} in
id ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘
typ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ ┴
doc └┘
547 begin
st └─────
548 rw [pi_generate_from_eq],
id └─────────────────┘
src └──┘└─────────────────┘┴
typ └──┘└─────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────────┘└──
549 refine le_antisymm (generate_from_mono _) (le_generate_from _),
id └─────────┘ └────────────────┘ └──────────────┘
src └─────┘└─────────┘┴ └────────────────┘└──┘ └──────────────┘└─┘
typ └─────┘└─────────┘┴ └────────────────┘└──┘ └──────────────┘└─┘
doc └─────┘ ┴ └──┘ └─┘
txt └─────┘ ┴ └──┘ └─┘
par └─────┘ ┴ └──┘ └─┘
pid ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────────────────────────┘└─
550 exact assume s ⟨t, ht, eq⟩, ⟨t, finset.univ, by simp [ht, eq]⟩,
id ┴ └─────────┘ └┘ └┘
src └────┘ └──┘ └┘ └┘ └─┘ └┘└─────────┘└┘ ┴└────┘ └┘└┘┴┴
typ └────┘ └──┘┴└┘ └┘ └─┘ └┘└─────────┘└┘ ┴└────┘└┘└┘└┘┴┴
doc └────┘ └──┘ └┘ └┘ └─┘ └┘└─────────┘└┘ ┴└────┘ └┘ ┴┴
txt └────┘ └──┘ └┘ └┘ └─┘ └┘ └┘ ┴└────┘ └┘ ┴┴
par └────┘ └──┘ └┘ └┘ └─┘ └┘ └┘ ┴└────┘ └┘ ┴┴
pid ┴ └──┘ └┘ └┘ └─┘ └┘ └┘ └─────┘ └┘ └┘
st ────────────────────────────────────────────────┘└────────────┘┴└─
551 { rintros s ⟨t, i, ht, rfl⟩,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └────────────────┘
st ────────────────────────────┘└─
552 apply is_open_iff_forall_mem_open.2 _,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└──┘
typ └────┘└─────────────────────────┘└──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴ └──┘
st ────────────────────────────────────────┘└─
553 assume f hf,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
554 choose c hc using show ∀a, ∃s, s ∈ g a ∧ f a ∈ s,
id ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴ ┴┴┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
typ └────────────────┘ ┴ ┴ ┴┴┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴ └─
doc └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid └┘└─┘└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────
555 { assume a, have : f a ∈ ⋃₀ g a, { rw [hg], apply mem_univ }, simpa },
id ┴ └┘ ┴ ┴ └┘ └──────┘
src ─────┘└──────┘└┘└─────┘ ┴ ┴ ┴└┘┴ ┴ └──┘└──┘ ┴└┘└────┘└──────┘┴└─┘└────┘┴
typ ─────┘└──────┘└┘└─────┘┴┴ ┴ ┴└┘┴┴┴┴└──┘└──┘└┘┴└┘└────┘└──────┘┴└─┘└────┘┴
doc ─────┘└──────┘└┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘└──┘ ┴└┘└────┘ ┴└─┘└────┘┴
txt ─────┘└──────┘└┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘└──┘ ┴└┘└────┘ ┴└─┘└────┘┴
par ─────┘└──────┘└┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘└──┘ ┴└┘└────┘ ┴└─┘└────┘┴
pid ──────────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └───────┘ └─────────┘
st ────┘└───────┘└───────────────────┘└─┘└─────┘└────────────────┘┴└──────┘└┘└
556 refine ⟨pi univ (λa, if a ∈ i then t a else (c : Πa, set (π a)) a), _, _, _⟩,
id └┘ └──┘ ┴ ┴ ┴ └─┘ ┴
src └─────┘ └┘┴└──┘┴ └─┘ └─┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴└─┘┴ ┴ └─┘ └─────────┘
typ └─────┘ └┘┴└──┘┴ └─┘ └─┘ ┴┴└────┘┴┴ └────┘ ┴└─┘ ┴ ┴└─┘┴ ┴┴ └─┘ └─────────┘
doc └─────┘ └┘┴ ┴ └─┘ └─┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘
txt └─────┘ ┴ ┴ └─┘ └─┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘
par └─────┘ ┴ ┴ └─┘ └─┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
557 { simp [pi_if] },
id └───┘
src └────┘└───┘└┘
typ └────┘└───┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ─────┘└───────────┘└┘└
558 { refine generate_open.basic _ ⟨_, assume a, _, rfl⟩,
id └─────────────────┘ └─┘
src └─────┘└─────────────────┘└─┘ └─┘ └─────┘└─┘┴
typ └─────┘└─────────────────┘└─┘ └─┘ └─────┘└─┘┴
doc └─────┘ └─┘ └─┘ └─────┘ ┴
txt └─────┘ └─┘ └─┘ └─────┘ ┴
par └─────┘ └─┘ └─┘ └─────┘ ┴
pid ┴ └─┘ └─┘ └─────┘ ┴
st ─────┘└────────────────────────────────────────────────┘└─
559 by_cases a ∈ i; simp [*, pi] at * },
id ┴ ┴ └┘
src └───────┘ ┴ ┴ └───────┘└┘└─────┘
typ └───────┘┴┴ ┴┴ └───────┘└┘└─────┘
doc └───────┘ ┴ ┴ └───────┘└┘└─────┘
txt └───────┘ ┴ ┴ └───────┘ └─────┘
par └───────┘ ┴ ┴ └───────┘ └─────┘
pid ┴ ┴ ┴ ┴└──┘ ┴┴└──┘┴
st ───────────────────────────────────────┘└┘└
560 { have : f ∈ pi {a | a ∉ i} c, { simp [*, pi] at * },
id ┴ └┘ ┴ ┴ ┴ └┘
src └─────┘ ┴ ┴└┘┴┴└──┘ ┴ ┴ └┘ └───────┘└┘└─────┘
typ └─────┘┴┴ ┴└┘┴┴└──┘ ┴ ┴┴└┘┴ └───────┘└┘└─────┘
doc └─────┘ ┴ ┴└┘┴ └──┘ ┴ ┴ └┘ └───────┘└┘└─────┘
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───────┘ └─────┘
par └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───────┘ └─────┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴└──┘ ┴┴└──┘┴
st ────────────────────────────────┘└──┘└────────────────┘└┘└
561 simpa [pi_if, hf] } }
id └───┘ └┘
src └─────┘└───┘└┘ └┘
typ └─────┘└───┘└┘└┘└┘
doc └─────┘ └┘ └┘
txt └─────┘ └┘ └┘
par └─────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────────────┘└───
562 end
st ──┘
563
564 end pi
565
566 section sigma
567 variables {ι : Type*} {σ : ι → Type*} [Π i, topological_space (σ i)]
id ┴ ┴ └───────────────┘ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴
doc └───────────────┘
568 open lattice
569
570 lemma continuous_sigma_mk {i : ι} : continuous (@sigma.mk ι σ i) :=
id ┴ └────────┘ └──────┘ ┴ ┴ ┴
src └────────┘ └──────┘
typ ┴ └────────┘ └──────┘ ┴ ┴ ┴
doc └────────┘
571 continuous_supr_rng continuous_coinduced_rng
id └─────────────────┘ └──────────────────────┘
src └─────────────────┘ └──────────────────────┘
typ └─────────────────┘ └──────────────────────┘
572
573 lemma is_open_sigma_iff {s : set (sigma σ)} : is_open s ↔ ∀ i, is_open (sigma.mk i ⁻¹' s) :=
id └─┘ └───┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ └─┘ ┴
src └─┘ └───┘ └─────┘ ┴ └─────┘ └──────┘ └─┘
typ └─┘ └───┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ └─┘ ┴
doc └─────┘ └─────┘ └─┘
574 by simp only [is_open_supr_iff, is_open_coinduced]
id └──────────────┘ └───────────────┘
src └─────────┘└──────────────┘└┘└───────────────┘└─
typ └─────────┘└──────────────┘└┘└───────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────────
575
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
576 lemma is_closed_sigma_iff {s : set (sigma σ)} : is_closed s ↔ ∀ i, is_closed (sigma.mk i ⁻¹' s) :=
id └─┘ └───┘ ┴ └───────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴ └─┘ ┴
src └─┘ └───┘ └───────┘ ┴ └───────┘ └──────┘ └─┘
typ └─┘ └───┘ ┴ └───────┘ ┴ ┴ ┴ └───────┘ └──────┘ ┴ └─┘ ┴
doc └───────┘ └───────┘ └─┘
577 is_open_sigma_iff
id └───────────────┘
src └───────────────┘
typ └───────────────┘
578
579 lemma is_open_map_sigma_mk {i : ι} : is_open_map (@sigma.mk ι σ i) :=
id ┴ └─────────┘ └──────┘ ┴ ┴ ┴
src └─────────┘ └──────┘
typ ┴ └─────────┘ └──────┘ ┴ ┴ ┴
doc └─────────┘
580 begin
st └─────
581 intros s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
582 rw is_open_sigma_iff,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────┘└─
583 intro j,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
584 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
585 by_cases h : i = j,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────┘└─
586 { subst j,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────┘└─
587 convert hs,
id └┘
src └──────┘
typ └──────┘└┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────────┘└─
588 exact set.preimage_image_eq _ injective_sigma_mk },
id └───────────────────┘ └────────────────┘
src └────┘└───────────────────┘└─┘└────────────────┘┴
typ └────┘└───────────────────┘└─┘└────────────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────────────────────────────┘└┘└
589 { convert is_open_empty,
id └───────────┘
src └──────┘└───────────┘
typ └──────┘└───────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────────────────┘└─
590 apply set.eq_empty_of_subset_empty,
id └──────────────────────────┘
src └────┘└──────────────────────────┘
typ └────┘└──────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────┘└─
591 rintro x ⟨y, _, hy⟩,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ──────────────────────┘└─
592 have : i = j, by cc,
id ┴ ┴
src └─────┘ ┴ ┴ └┘
typ └─────┘┴┴ ┴┴ └┘
doc └─────┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴
st ───────────────┘ └─
593 contradiction }
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────┘└─
594 end
st ──┘
595
596 lemma is_open_range_sigma_mk {i : ι} : is_open (set.range (@sigma.mk ι σ i)) :=
id ┴ └─────┘ └───────┘ └──────┘ ┴ ┴ ┴
src └─────┘ └───────┘ └──────┘
typ ┴ └─────┘ └───────┘ └──────┘ ┴ ┴ ┴
doc └─────┘ └───────┘
597 by { rw ←set.image_univ, exact is_open_map_sigma_mk _ is_open_univ }
id └────────────┘ └──────────────────┘ └──────────┘
src └──┘└────────────┘ └────┘└──────────────────┘└─┘└──────────┘┴
typ └──┘└────────────┘ └────┘└──────────────────┘└─┘└──────────┘┴
doc └──┘ └────┘ └─┘ ┴
txt └──┘ └────┘ └─┘ ┴
par └──┘ └────┘ └─┘ ┴
pid └┘ ┴ └─┘ ┴
st └───────────────────┘└──────────────────────────────────────────┘└┘
598
599 lemma is_closed_map_sigma_mk {i : ι} : is_closed_map (@sigma.mk ι σ i) :=
id ┴ └───────────┘ └──────┘ ┴ ┴ ┴
src └───────────┘ └──────┘
typ ┴ └───────────┘ └──────┘ ┴ ┴ ┴
600 begin
st └─────
601 intros s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
602 rw is_closed_sigma_iff,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
603 intro j,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
604 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
605 by_cases h : i = j,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────┘└─
606 { subst j,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────┘└─
607 convert hs,
id └┘
src └──────┘
typ └──────┘└┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────────┘└─
608 exact set.preimage_image_eq _ injective_sigma_mk },
id └───────────────────┘ └────────────────┘
src └────┘└───────────────────┘└─┘└────────────────┘┴
typ └────┘└───────────────────┘└─┘└────────────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────────────────────────────┘└┘└
609 { convert is_closed_empty,
id └─────────────┘
src └──────┘└─────────────┘
typ └──────┘└─────────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────────────────┘└─
610 apply set.eq_empty_of_subset_empty,
id └──────────────────────────┘
src └────┘└──────────────────────────┘
typ └────┘└──────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────┘└─
611 rintro x ⟨y, _, hy⟩,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ──────────────────────┘└─
612 have : i = j, by cc,
id ┴ ┴
src └─────┘ ┴ ┴ └┘
typ └─────┘┴┴ ┴┴ └┘
doc └─────┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴
st ───────────────┘ └─
613 contradiction }
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────┘└─
614 end
st ──┘
615
616 lemma is_closed_sigma_mk {i : ι} : is_closed (set.range (@sigma.mk ι σ i)) :=
id ┴ └───────┘ └───────┘ └──────┘ ┴ ┴ ┴
src └───────┘ └───────┘ └──────┘
typ ┴ └───────┘ └───────┘ └──────┘ ┴ ┴ ┴
doc └───────┘ └───────┘
617 by { rw ←set.image_univ, exact is_closed_map_sigma_mk _ is_closed_univ }
id └────────────┘ └────────────────────┘ └────────────┘
src └──┘└────────────┘ └────┘└────────────────────┘└─┘└────────────┘┴
typ └──┘└────────────┘ └────┘└────────────────────┘└─┘└────────────┘┴
doc └──┘ └────┘ └─┘ ┴
txt └──┘ └────┘ └─┘ ┴
par └──┘ └────┘ └─┘ ┴
pid └┘ ┴ └─┘ ┴
st └───────────────────┘└──────────────────────────────────────────────┘└┘
618
619 lemma open_embedding_sigma_mk {i : ι} : open_embedding (@sigma.mk ι σ i) :=
id ┴ └────────────┘ └──────┘ ┴ ┴ ┴
src └────────────┘ └──────┘
typ ┴ └────────────┘ └──────┘ ┴ ┴ ┴
doc └────────────┘
620 open_embedding_of_continuous_injective_open
id └─────────────────────────────────────────┘
src └─────────────────────────────────────────┘
typ └─────────────────────────────────────────┘
621 continuous_sigma_mk injective_sigma_mk is_open_map_sigma_mk
id └─────────────────┘ └────────────────┘ └──────────────────┘
src └─────────────────┘ └────────────────┘ └──────────────────┘
typ └─────────────────┘ └────────────────┘ └──────────────────┘
622
623 lemma closed_embedding_sigma_mk {i : ι} : closed_embedding (@sigma.mk ι σ i) :=
id ┴ └──────────────┘ └──────┘ ┴ ┴ ┴
src └──────────────┘ └──────┘
typ ┴ └──────────────┘ └──────┘ ┴ ┴ ┴
doc └──────────────┘
624 closed_embedding_of_continuous_injective_closed
id └─────────────────────────────────────────────┘
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘
625 continuous_sigma_mk injective_sigma_mk is_closed_map_sigma_mk
id └─────────────────┘ └────────────────┘ └────────────────────┘
src └─────────────────┘ └────────────────┘ └────────────────────┘
typ └─────────────────┘ └────────────────┘ └────────────────────┘
626
627 lemma embedding_sigma_mk {i : ι} : embedding (@sigma.mk ι σ i) :=
id ┴ └───────┘ └──────┘ ┴ ┴ ┴
src └───────┘ └──────┘
typ ┴ └───────┘ └──────┘ ┴ ┴ ┴
doc └───────┘
628 closed_embedding_sigma_mk.1
id └───────────────────────┘┴
src └───────────────────────┘┴
typ └───────────────────────┘┴
629
630 /-- A map out of a sum type is continuous if its restriction to each summand is. -/
631 lemma continuous_sigma [topological_space β] {f : sigma σ → β}
id └───────────────┘ ┴ └───┘ ┴ ┴
src └───────────────┘ └───┘
typ └───────────────┘ ┴ └───┘ ┴ ┴
doc └───────────────┘
632 (h : ∀ i, continuous (λ a, f ⟨i, a⟩)) : continuous f :=
id ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
633 continuous_supr_dom (λ i, continuous_coinduced_dom (h i))
id └─────────────────┘ ┴ └──────────────────────┘ ┴ ┴
src └─────────────────┘ └──────────────────────┘
typ └─────────────────┘ ┴ └──────────────────────┘ ┴ ┴
634
635 lemma continuous_sigma_map {κ : Type*} {τ : κ → Type*} [Π k, topological_space (τ k)]
id ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘
636 {f₁ : ι → κ} {f₂ : Π i, σ i → τ (f₁ i)} (hf : ∀ i, continuous (f₂ i)) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ └┘ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ └┘ ┴
doc └────────┘
637 continuous (sigma.map f₁ f₂) :=
id └────────┘ └───────┘ └┘ └┘
src └────────┘ └───────┘
typ └────────┘ └───────┘ └┘ └┘
doc └────────┘ └───────┘
638 continuous_sigma $ λ i,
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
doc └──────────────┘
639 show continuous (λ a, sigma.mk (f₁ i) (f₂ i a)),
id └────────┘ ┴ └──────┘ └┘ ┴ └┘ ┴ ┴
src └────────┘ └──────┘
typ └────────┘ ┴ └──────┘ └┘ ┴ └┘ ┴ ┴
doc └────────┘
640 from continuous_sigma_mk.comp (hf i)
id └─────────────────┘└───┘ └┘ ┴
src └─────────────────┘└───┘
typ └─────────────────┘└───┘ └┘ ┴
641
642 lemma is_open_map_sigma [topological_space β] {f : sigma σ → β}
id └───────────────┘ ┴ └───┘ ┴ ┴
src └───────────────┘ └───┘
typ └───────────────┘ ┴ └───┘ ┴ ┴
doc └───────────────┘
643 (h : ∀ i, is_open_map (λ a, f ⟨i, a⟩)) : is_open_map f :=
id ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
644 begin
st └─────
645 intros s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
646 rw is_open_sigma_iff at hs,
id └───────────────┘
src └─┘└───────────────┘└────┘
typ └─┘└───────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ───────────────────────────┘└─
647 have : s = ⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s),
id ┴ ┴ ┴ └┘ └──────┘ └─┘ ┴
src └─────┘ ┴┴┴┴└┘┴┴ ┴ ┴└┘┴ └──────┘┴ ┴└─┘┴ ┴
typ └─────┘ ┴┴┴┴└┘┴┴ ┴ ┴└┘┴ └──────┘┴ ┴└─┘┴┴┴
doc └─────┘ ┴ ┴┴└┘┴┴ ┴ ┴ ┴ ┴ ┴└─┘┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
648 { rw Union_image_preimage_sigma_mk_eq_self },
id └───────────────────────────────────┘
src └─┘└───────────────────────────────────┘┴
typ └─┘└───────────────────────────────────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───┘└───────────────────────────────────────┘└┘└
649 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
650 rw [image_Union],
id └─────────┘
src └──┘└─────────┘┴
typ └──┘└─────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────┘└──
651 apply is_open_Union,
id └───────────┘
src └────┘└───────────┘
typ └────┘└───────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
652 intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
653 rw [image_image],
id └─────────┘
src └──┘└─────────┘┴
typ └──┘└─────────┘┴
doc └──┘└─────────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────┘└──
654 exact h i _ (hs i)
id ┴ └┘ ┴
src └────┘ ┴ └─┘ ┴ └┘
typ └────┘┴┴ └─┘ └┘┴┴└┘
doc └────┘ ┴ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └┘
par └────┘ ┴ └─┘ ┴ └┘
pid ┴ ┴ └─┘ ┴ ┴┴
st ────────────────────┘
655 end
st └─┘
656
657 /-- The sum of embeddings is an embedding. -/
658 lemma embedding_sigma_map {τ : ι → Type*} [Π i, topological_space (τ i)]
id ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘
659 {f : Π i, σ i → τ i} (hf : ∀ i, embedding (f i)) : embedding (sigma.map id f) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ └───────┘ └┘ ┴
src └───────┘ └───────┘ └───────┘ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ └───────┘ └┘ ┴
doc └───────┘ └───────┘ └───────┘
660 begin
st └─────
661 refine ⟨⟨_⟩, injective_sigma_map function.injective_id (λ i, (hf i).inj)⟩,
id └─────────────────┘ └───────────────────┘ └┘
src └─────┘ └──┘└─────────────────┘┴└───────────────────┘┴ └──┘ ┴ └─────┘
typ └─────┘ └──┘└─────────────────┘┴└───────────────────┘┴ └──┘ └┘┴ └─────┘
doc └─────┘ └──┘ ┴ ┴ └──┘ ┴ └─────┘
txt └─────┘ └──┘ ┴ ┴ └──┘ ┴ └─────┘
par └─────┘ └──┘ ┴ ┴ └──┘ ┴ └─────┘
pid ┴ └──┘ ┴ ┴ └──┘ ┴ └─────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
662 refine le_antisymm
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────
663 (continuous_iff_le_induced.mp (continuous_sigma_map (λ i, (hf i).continuous))) _,
id └──────────────────────────┘ └──────────────────┘ └┘
src ───┘ └──────────────────────────┘┴ └──────────────────┘┴ └──┘ ┴ └───────────────┘
typ ───┘ └──────────────────────────┘┴ └──────────────────┘┴ └──┘ └┘┴ └───────────────┘
doc ───┘ ┴ ┴ └──┘ ┴ └───────────────┘
txt ───┘ ┴ ┴ └──┘ ┴ └───────────────┘
par ───┘ ┴ ┴ └──┘ ┴ └───────────────┘
pid ───┘ ┴ ┴ └──┘ ┴ └───────────────┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
664 intros s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
665 replace hs := is_open_sigma_iff.mp hs,
id └──────────────────┘ └┘
src └────────────┘└──────────────────┘┴
typ └────────────┘└──────────────────┘┴└┘
doc └────────────┘ ┴
txt └────────────┘ ┴
par └────────────┘ ┴
pid └─┘┴└─┘ ┴
st ──────────────────────────────────────┘└─
666 have : ∀ i, ∃ t, is_open t ∧ f i ⁻¹' t = sigma.mk i ⁻¹' s,
id ┴ ┴ └─────┘ ┴ └─┘ ┴ └──────┘ ┴
src └─────┘ └┘ ┴┴└┘┴┴└─────┘┴ ┴ ┴ ┴ ┴└─┘┴ ┴┴┴└──────┘┴ ┴ ┴
typ └─────┘ └┘ ┴┴└┘┴┴└─────┘┴ ┴ ┴┴┴ ┴└─┘┴ ┴┴┴└──────┘┴ ┴ ┴┴
doc └─────┘ └┘ ┴ └┘ ┴└─────┘┴ ┴ ┴ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
667 { intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
668 apply is_open_induced_iff.mp,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
669 convert hs i,
id └┘ ┴
src └──────┘ ┴
typ └──────┘└┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ───────────────┘└─
670 exact (hf i).induced.symm },
id └┘ ┴
src └────┘ ┴ └─────────────┘
typ └────┘ └┘┴┴└─────────────┘
doc └────┘ ┴ └─────────────┘
txt └────┘ ┴ └─────────────┘
par └────┘ ┴ └─────────────┘
pid ┴ ┴ └───────────┘└┘
st ─────────────────────────────┘└┘└
671 choose t ht using this,
id └──┘
src └────────────────┘
typ └────────────────┘└──┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘└─┘└─────┘
st ───────────────────────┘└─
672 apply is_open_induced_iff.mpr,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
673 refine ⟨⋃ i, sigma.mk i '' t i, is_open_Union (λ i, is_open_map_sigma_mk _ (ht i).1), _⟩,
id ┴ ┴ └──────┘ └┘ ┴ └───────────┘ └──────────────────┘ └┘
src └─────┘ ┴└┘┴┴└──────┘┴ ┴└┘┴ ┴ └┘└───────────┘┴ └──┘└──────────────────┘└─┘ ┴ └──────┘
typ └─────┘ ┴└┘┴┴└──────┘┴ ┴└┘┴┴┴ └┘└───────────┘┴ └──┘└──────────────────┘└─┘ └┘┴ └──────┘
doc └─────┘ ┴└┘┴┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ └──────┘
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ └──────┘
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ └──────┘
pid ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ └──────┘
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
674 ext p,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
675 rcases p with ⟨i, x⟩,
id ┴
src └─────┘ └──────────┘
typ └─────┘┴└──────────┘
doc └─────┘ └──────────┘
txt └─────┘ └──────────┘
par └─────┘ └──────────┘
pid ┴ └──────────┘
st ─────────────────────┘└─
676 change (sigma.mk i (f i x) ∈ ⋃ (i : ι), sigma.mk i '' t i) ↔ x ∈ sigma.mk i ⁻¹' s,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ └┘┴┴┴└────┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──────┘┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴┴ ┴ └┘┴┴┴└────┘┴┴┴┴ ┴ ┴ ┴┴┴ └┘ ┴┴┴ ┴└──────┘┴┴┴ ┴┴
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴┴└────┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
677 rw [←(ht i).2, mem_Union],
id └┘ ┴ └───────┘
src └───┘ ┴ └───┘└───────┘┴
typ └───┘ └┘┴┴└───┘└───────┘┴
doc └───┘ ┴ └───┘ ┴
txt └───┘ ┴ └───┘ ┴
par └───┘ ┴ └───┘ ┴
pid └─┘ ┴ └───┘ ┴
st ────────────┘└───────────┘└──
678 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
679 { rintro ⟨j, hj⟩,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
680 rw mem_image at hj,
id └───────┘
src └─┘└───────┘└────┘
typ └─┘└───────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ─────────────────────┘└─
681 rcases hj with ⟨y, hy₁, hy₂⟩,
id └┘
src └─────┘ └─────────────────┘
typ └─────┘└┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ───────────────────────────────┘└─
682 rcases sigma.mk.inj_iff.mp hy₂ with ⟨rfl, hy⟩,
id └─────────────────┘ └─┘
src └─────┘└─────────────────┘┴ └─────────────┘
typ └─────┘└─────────────────┘┴└─┘└─────────────┘
doc └─────┘ ┴ └─────────────┘
txt └─────┘ ┴ └─────────────┘
par └─────┘ ┴ └─────────────┘
pid ┴ ┴ └─────────────┘
st ────────────────────────────────────────────────┘└─
683 replace hy := eq_of_heq hy,
id └───────┘ └┘
src └────────────┘└───────┘┴
typ └────────────┘└───────┘┴└┘
doc └────────────┘ ┴
txt └────────────┘ ┴
par └────────────┘ ┴
pid └─┘┴└─┘ ┴
st ─────────────────────────────┘└─
684 subst y,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
685 exact hy₁ },
id └─┘
src └────┘ ┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────┘└┘└
686 { intro hx,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ───────────┘└─
687 use i,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ────────┘└─
688 rw mem_image,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
689 exact ⟨f i x, hx, rfl⟩ }
id ┴ ┴ ┴ └┘ └─┘
src └────┘ ┴ ┴ └┘ └┘└─┘└┘
typ └────┘ ┴┴┴┴┴└┘└┘└┘└─┘└┘
doc └────┘ ┴ ┴ └┘ └┘ └┘
txt └────┘ ┴ ┴ └┘ └┘ └┘
par └────┘ ┴ ┴ └┘ └┘ └┘
pid ┴ ┴ ┴ └┘ └┘ ┴┴
st ──────────────────────────┘└─
690 end
st ──┘
691
692 end sigma
693
694 lemma mem_closure_of_continuous [topological_space α] [topological_space β]
id └───────────────┘ ┴ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘
695 {f : α → β} {a : α} {s : set α} {t : set β}
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
696 (hf : continuous f) (ha : a ∈ closure s) (h : ∀a∈s, f a ∈ closure t) :
id └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └────────┘ ┴ └─────┘ ┴ └─────┘
typ └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └────────┘ └─────┘ └─────┘
697 f a ∈ closure t :=
id ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
698 calc f a ∈ f '' closure s : mem_image_of_mem _ ha
id ┴ ┴ ┴ └┘ └─────┘ ┴ └──────────────┘ └┘
src └┘ └─────┘ └──────────────┘
typ ┴ ┴ ┴ └┘ └─────┘ ┴ └──────────────┘ └┘
doc └─────┘
699 ... ⊆ closure (f '' s) : image_closure_subset_closure_image hf
id └─────┘ ┴ └┘ ┴ └────────────────────────────────┘ └┘
src └─────┘ └┘ └────────────────────────────────┘
typ └─────┘ ┴ └┘ ┴ └────────────────────────────────┘ └┘
doc └─────┘
700 ... ⊆ closure (closure t) : closure_mono $ image_subset_iff.mpr $ h
id └─────┘ └─────┘ ┴ └──────────┘ └──────────────┘└──┘ ┴
src └─────┘ └─────┘ └──────────┘ └──────────────┘└──┘
typ └─────┘ └─────┘ ┴ └──────────┘ └──────────────┘└──┘ ┴
doc └─────┘ └─────┘ └──────────────┘
701 ... ⊆ closure t : begin rw [closure_eq_of_is_closed], exact subset.refl _, exact is_closed_closure end
id └─────┘ ┴ └─────────────────────┘ └─────────┘ └───────────────┘
src └─────┘ └──┘└─────────────────────┘┴ └────┘└─────────┘└┘ └────┘└───────────────┘┴
typ └─────┘ ┴ └──┘└─────────────────────┘┴ └────┘└─────────┘└┘ └────┘└───────────────┘┴
doc └─────┘ └──┘ ┴ └────┘ └┘ └────┘ ┴
txt └──┘ ┴ └────┘ └┘ └────┘ ┴
par └──┘ ┴ └────┘ └┘ └────┘ ┴
pid └┘ ┴ ┴ └┘ ┴ ┴
st └───────────────────────────────┘└────────────────────┘└────────────────────────┘└─┘
702
703 lemma mem_closure_of_continuous2 [topological_space α] [topological_space β] [topological_space γ]
id └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴
src └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘ └───────────────┘
704 {f : α → β → γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ}
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ ┴
705 (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
id └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
src └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────┘
typ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
doc └────────┘ └─────┘ └─────┘
706 (h : ∀a∈s, ∀b∈t, f a b ∈ closure u) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
707 f a b ∈ closure u :=
id ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
708 have (a,b) ∈ closure (set.prod s t),
id ┴┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴
src ┴ ┴ └─────┘ └──────┘
typ ┴┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴
doc └─────┘ └──────┘
709 by simp [closure_prod_eq, ha, hb],
id └─────────────┘ └┘ └┘
src └────┘└─────────────┘└┘ └┘ ┴
typ └────┘└─────────────┘└┘└┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └─────────────────────────────┘
710 show f (a, b).1 (a, b).2 ∈ closure u,
id ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
711 from @mem_closure_of_continuous (α×β) _ _ _ (λp:α×β, f p.1 p.2) (a,b) _ u hf this $
id └───────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └┘ └──┘
src └───────────────────────┘ ┴ ┴ ┴ ┴ ┴
typ └───────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴ └┘ └──┘
712 assume ⟨p₁, p₂⟩ ⟨h₁, h₂⟩, h p₁ h₁ p₂ h₂
id ┴└┘ └┘ ┴└┘ └┘ ┴
typ ┴└┘ └┘ ┴└┘ └┘ ┴